(* the systems [LR->] and [LRt->] ("sb" = Square Brackets) *) (* some definitions in bddefs.thy, bdseq.thy *) (* need to prove equivalence of systems, should be able to prove inductively that if As |- B is provable in LRi then anything between As |- B and singles As |- B is provable in LRisb *) (* cut-admissibility *) (* note if multicut is admissible, then multicutting with {#A#} |- A gives contraction of A *) (* contraction admissibility of LRisb *) val _ = qed_goal_spec_mp "gsc_id" LRisb.thy "gen_step (lcd rls) A any drs ([], {#Aa#} |- Aa)" (fn _ => [ (simp_tac (esimps [gen_step.simps, lcd, lca, single_is_union]) 1) ]) ; val _ = qed_goal_spec_mp "gsc_tR" LRisb.thy "gen_step (lcd rls) A any drs ([], {#} |- X)" (fn _ => [ (simp_tac (esimps [gen_step.simps, lcd, lca]) 1) ]) ; val _ = qed_goal_spec_mp "gsc_tL" LRisb.thy "tL <= rls --> gen_step (lcd rls) A any (derrec rls {}) \ \ ([alpha |- B], mins T alpha |- B)" (fn _ => [ (simp_tac (esimps [gen_step.simps, lcd, lca]) 1), Safe_tac, (thin_tac "All ?P" 1), (case_tac "A = T" 1), (force_tac (cesimps [mins_def']) 1), (clarsimp_tac (cds [ms_split_sum], esimps [mins_def', single_is_union]) 1), Safe_tac, ALLGOALS Clarsimp_tac, (dtac (transfer LRisb.thy tL.I RS rev_subsetD RS drs.derI'') 1), Clarsimp_tac 1, (chop_tac 1 (atac 1)), (full_simp_tac (esimps (mins_def :: union_ac)) 1) ]) ; val _ = qed_goal_spec_mp "gsc_impR" LRisb.thy "impR <= rls --> gen_step (lcd rls) C any (derrec rls {}) \ \ ([mins A alpha |- B], alpha |- A -> B)" (fn _ => [ (simp_tac (esimps [gen_step.simps, lcd, lca]) 1), Safe_tac, (thin_tac "All ?P" 1), (etac allE 1), (etac impE 1), MSSG (simp_tac (esimps [mins_assoc RS sym])) 1, (full_simp_tac (esimps [mins_assoc]) 1), (etac (transfer LRisb.thy impR.I RS rev_subsetD RS drs.derI'') 1), Simp_tac 1 ]) ; (* goal LRisb.thy "Y + {#D#} : sqbr AB (mins AB alpha + beta) --> \ \ Y ~: sqbr AB (mins AB alpha + beta) --> \ \ count (alpha + beta) D = Suc (Suc (count Y D))" ; (clarify_tac (ces sqbr.elims) 1), etac swap 1, rtac sqbr.I 1, etac xt6 1, MSSG Simp_tac 1, Clarify_tac 1, (datac bspec 1 1), mp_tac 1, (case_tac "D = fml" 1), (force_tac (cesimps [count_mins]) 1), Force_tac 1, (case_tac "D = AB" 1), Force_tac 2, (clarsimp_tac (cesimps [count_mins]) 1), rtac xt6 1, atac 2, (clarsimp_tac (cesimps [count_mins, ms_le_def]) 1), (eres_inst_tac [("x", "D")] allE 1) *) val _ = qed_goal_spec_mp "gsc_sbimpL" LRisb.thy "sbimpL <= rls --> cms : sqbr (A -> B) (mins (A -> B) alpha + beta) --> \ \ gen_step (lcd rls) D any (derrec rls {}) \ \ ([alpha |- A, mins B beta |- C], cms |- C)" (fn _ => [ (simp_tac (esimps [gen_step.simps, lcd, lca]) 1), Safe_tac, (thin_tac "All ?P" 1), (case_tac "X + {#D#} : sqbr (A -> B) (mins (A -> B) alpha + beta)" 1), (eatac (transfer LRisb.thy sbimpL.I RS rev_subsetD RS drs.derI'') 1 1), Force_tac 1,