(* this file is largely unchanged from the set version, found in ../seqsem, and doesn't work *) val () = qed_goal_spec_mp "car_lmono" calk.thy "(X |- Y, x) : car lkss A --> X <= X' --> Y <= Y' --> \ \ (X' |- Y', x) : car lkss A" (fn _ => [ (case_tac "x" 1), (asm_simp_tac (esimps [car_eq]) 1), Safe_tac, (etac lkw 1), Asm_simp_tac 1, etac le_sub 1]) ; val () = qed_goal_spec_mp "car_rmono" calk.thy "(x, X |- Y) : car lkss A --> X <= X' --> Y <= Y' --> \ \ (x, X' |- Y') : car lkss A" (fn _ => [ (case_tac "x" 1), (asm_simp_tac (esimps [car_eq]) 1), Safe_tac, (etac lkw 1), Asm_simp_tac 1, etac le_sub 1]) ; val car_wk = transfer calk.thy carD RS lkw RS car.caI ; val ltod1s = lkne.intros RL [lkss.extI RS transfer calk.thy drl.singleI'] ; val ltod2s = map (simplify (esimps [])) ltod1s ; val ltod3s = map (full_simplify (esimps [])) ([ltod2s, [dersl_all RS iffD2]] MRL [derl_trans]) ; fun toco rl = case map (full_simplify (esimps [])) ([rl] RL ltod3s) of [res] => tacthm (TRY Safe_tac) res | _ => raise THM ("toco", 0, [rl]) ; (* val thar2' = prove_goal calk.thy "(X |- mins A (mins B Y), mins A X |- Y) : car lkss A --> \ \ (X |- mins B Y) : derrec lkss {}" (fn _ => [ Safe_tac, (dtac carD 1), (etac lkw 1), Auto_tac]) ; val thbr2' = prove_goal calk.thy "(X |- mins A Y, mins A (mins B X) |- Y) : car lkss A --> \ \ ((mins B X) |- Y) : derrec lkss {}" (fn _ => [ Safe_tac, (dtac carD 1), (etac lkw 1), Auto_tac]) ; (* NOTE - first two premises not needed for proofs of these *) val [thar2, thbr2] = map (rewrite_rule [drr_empty] o rotate_prems 1) ([car_cas RS cas_car] RL ([thar2', thbr2'] RL [mp])) ; val dt1 = Dtree (icrms, [Dleaf]) ; val dt2 = Dtree (toco lkil.andl1, [Dleaf]) ; val dt3 = Dtree (thar2, [dt1, dt2]) ; val dt4 = Dtree (toco lkir.andr, [Dleaf, Dleaf]) ; val dt5 = Dtree (iclms, [Dleaf]) ; val dt6 = Dtree (thbr2, [dt4, dt5]) ; val dt7 = Dtree (carDl, [dt3, dt6]) ; val pr_and1 = calcDT dt7 ; val dt2 = Dtree (toco lkil.andl2, [Dleaf]) ; val dt3 = Dtree (thar2, [dt1, dt2]) ; val dt7 = Dtree (carDl, [dt3, dt6]) ; val pr_and2 = calcDT dt7 ; val dt1 = Dtree (iclms, [Dleaf]) ; val dt2 = Dtree (toco lkir.orr1, [Dleaf]) ; val dt3 = Dtree (thbr2, [dt1, dt2]) ; val dt4 = Dtree (toco lkil.orl, [Dleaf, Dleaf]) ; val dt5 = Dtree (icrms, [Dleaf]) ; val dt6 = Dtree (thar2, [dt4, dt5]) ; val dt7 = Dtree (carDl, [dt3, dt6]) ; val pr_or1 = calcDT (revDT dt7) ; val dt2 = Dtree (toco lkir.orr2, [Dleaf]) ; val dt3 = Dtree (thbr2, [dt1, dt2]) ; val dt7 = Dtree (carDl, [dt3, dt6]) ; val pr_or2 = calcDT (revDT dt7) ; *) (* pr_andi, pr_ori, not actually used any more *) (* using cas *) (* ; val prems = it ; *) (* note - proof of lcstep and rcstep does not depend on the actual rules, only the link between lkne and lkss, expressed in lkss.extI *) fun taccss subs = [ (rtac car.caI 1), (rtac drs.derI 1), (dres_inst_tac subs lkss.extI 1), (Full_simp_tac 1), (etac mem_same 1), (asm_simp_tac (esimps [diff_union_single_conv_ne] addsimprocs pmgsps) 1), (simp_tac (esimps [drs.all]) 1), (Clarify_tac 1), (case_tac "xa" 1), Asm_full_simp_tac 1, (datac bspec 1 1), Full_simp_tac 1, (dtac carD 1), (etac lkw 1), (simp_tac (esimps [pm_assoc_le] addsimprocs pmgsps) 1) ] ; val lcstep = prove_goal calk.thy "[| (ps, U |- V) : lkne ; ~ (A :# V) ; \ \ pse = map (extend (W |- Z)) ps ; \ \ (ALL p : set pse. (p, (X |- Y)) : car lkss A) |] ==> \ \ ((U + W |- V + Z), (X |- Y)) : car lkss A" (fn prems => (cut_facts_tac prems 1) :: (taccss [("flr", "W + (X - {#A#}) |- Z - {#A#} + Y")])) ; val rcstep = prove_goal calk.thy "[| (ps, U |- V) : lkne ; ~ (A :# U) ; \ \ pse = map (extend (W |- Z)) ps ; \ \ (ALL p : set pse. ((X |- Y), p) : car lkss A) |] ==> \ \ ((X |- Y), (U + W |- V + Z)) : car lkss A" (fn prems => (cut_facts_tac prems 1) :: (taccss [("flr", "X + (W - {#A#}) |- Z + (Y - {#A#})")])) ; (* ; val prems = it ; *) val ths = ([hd prod.inject, sequent.inject, singleton_insert_inj_eq] RL [iffD1 RS conjE]) ; fun tacips casd = [ (etac allE), etac impE, (REPEAT1 o etac allE o incr), (etac casd o incr), (resolve_tac ipsfIs THEN' atac THEN' atac) ] ; val prstep' = prove_goal calk.thy "(ps, {#} |- {#A#}) : lkir & (qs, {#A#} |- {#}) : lkil & \ \ pse = map (extend (X |- Y)) ps & qse = map (extend (U |- V)) qs & \ \ set pse Un set qse <= derrec lkss {} & \ \ (ALL p : set pse. (p, (mins A U |- V)) : car lkss A) & \ \ (ALL q : set qse. ((X |- mins A Y), q) : car lkss A) & \ \ (ALL sfa X Y U V. (sfa, A) : ipsubfml --> \ \ ((X |- mins sfa Y), (mins sfa U |- V)) : cas lkss sfa) --> \ \ ((X |- mins A Y), (mins A U |- V)) : cas lkss A" (fn _ => [ Safe_tac, (etac lkil.elims 1), (ALLGOALS (etac lkir.elims)), (ALLGOALS (REPEAT o eresolve_tac ths)), (ALLGOALS (REPEAT o dtac (single_eq_single RS iffD1))), (ALLGOALS (eresolve_tac fc2Es' THEN' atac)), (* avoid the following until most subgoals removed *) Safe_tac, (ALLGOALS Full_simp_tac), Safe_tac, (ALLGOALS (rtac casI')), (TRYALL (EVERY' (tacips casD''))), (TRYALL (EVERY' (tacips casD3))) ]) RS mp ; (* previous one val prstep' = prove_goal calk.thy "(ps, {#} |- {#A#}) : lkir & (qs, {#A#} |- {#}) : lkil & \ \ pse = map (extend (X |- Y)) ps & qse = map (extend (X |- Y)) qs & \ \ set pse Un set qse <= derrec lkss {} & \ \ (ALL p : set pse. (p, (mins A X |- Y)) : car lkss A) & \ \ (ALL q : set qse. ((X |- mins A Y), q) : car lkss A) & \ \ (ALL sfa. (sfa, A) : ipsubfml --> \ \ ((X |- mins sfa Y), (mins sfa X |- Y)) : cas lkss sfa) --> \ \ ((X |- mins A Y), (mins A X |- Y)) : cas lkss A" (fn _ => [ Safe_tac, (etac lkil.elims 1), (ALLGOALS (etac lkir.elims)), (ALLGOALS (REPEAT o eresolve_tac ths)), (ALLGOALS (REPEAT o dtac (single_eq_single RS iffD1))), (ALLGOALS (eresolve_tac fc2Es' THEN' atac)), (* avoid the following until most subgoals removed *) Safe_tac, (ALLGOALS Full_simp_tac), Safe_tac, (ALLGOALS (rtac casI')), (TRYALL (EVERY' tacips))]) RS mp ; *) val extend_lem1 = prove_goal cagen.thy "extend (X |- Y) (0 |- {#A#}) = (X |- mins A Y)" (fn _ => [ (simp_tac (esimps [extend_def, mins_def]) 1) ]) ; val extend_lem2 = prove_goal cagen.thy "extend (X |- Y) ({#A#} |- 0) = (mins A X |- Y)" (fn _ => [ (simp_tac (esimps [extend_def, mins_def]) 1) ]) ; val prstep = meta_std (prove_goal calk.thy "?P --> ?s : car lkss A" (fn _ => [ (rtac impI 1), (rtac cas_car 1), (etac prstep' 1), Safe_tac, (PRIMITIVE (fst o freeze_thaw o standard)), (REPEAT (EVERY' [ (rtac drs.derI), (REPEAT o (dresolve_tac lkne.intros)), (etac (lk_extI2 RS mem_same)), Simp_tac, (MSSG (REPEAT_ALL_NEW (resolve_tac [refl, conjI, extend_lem1, extend_lem2]))), (asm_full_simp_tac (esimps [drs.all]))] 1))])) ; val prstep_z = full_simplify (esimps []) prstep ; val caxtacs = [ (case_tac "seq" 1), hyp_subst_tac 1, (rtac casI 1), (case_tac "A = B" 1), (rtac lkw_ax 2), Force_tac 2, Force_tac 2 ] ; val rcxtacs = [ (etac lkw 1), (asm_simp_tac (esimps [mins_def] addsimprocs pmgsps) 1), (simp_tac (esimps [ms_le_def]) 1), arith_tac 1 ] ; val cas_axl = prove_goal calk.thy "(mins B U |- mins B V, seq) : cas lkss A" (fn _ => caxtacs @ etac thin_rl 1 :: rcxtacs) ; val cas_axr = prove_goal calk.thy "(seq, mins B U |- mins B V) : cas lkss A" (fn _ => caxtacs @ rcxtacs) ; val [car_axl, car_axr] = map (rewrite_rule [mins_def] o tacthm (TRYALL (match_tac [lk_axd]))) ([cas_axl, cas_axr] RL [cas_car]) ; val lcstep_cz = full_simplify (esimps []) lcstep ; val rcstep_cz = full_simplify (esimps []) rcstep ; val casitacs = [ (res_inst_tac [("x", "A")] formula_induct_subfml 1), Safe_tac, (rtac cas.caI 1), Safe_tac, (rename_tac "A X Y U V" 1), (eatac drs.induct2 1 1), (thin_tac "?s : ?S" 1), (REPEAT1 (etac lkss.elims 1)), (split_all_tac 1), (case_tac "b" 1), (case_tac "ba" 1), (case_tac "flr" 1), (case_tac "flra" 1), Safe_tac, (case_tac "A :# multiset2" 1), (* level 13 *) (* left commutative step *) (Full_simp_tac 2), Clarify_tac 2, (eatac (refl RSN (3, lcstep_cz)) 2 2), (case_tac "A :# multiset1a" 1), (* right commutative step *) (Full_simp_tac 2), Clarify_tac 2, (eatac (refl RSN (3, rcstep_cz)) 2 2), (etac lkne.elims 1), (* level 22 *) (* axiom on left *) (Asm_full_simp_tac 1), (eatac car_axl 1 1), (* left intro rule on left - contradiction *) (split_all_tac 1), (dtac lk_concl_ilc 1), Force_tac 1, (etac lkne.elims 1), (* axiom on right *) (Asm_full_simp_tac 1), (eatac car_axr 1 1), (* right intro rule on right - contradiction *) (split_all_tac 2), (REPEAT (dtac lk_concl_irc 2)), Force_tac 2, (* now for corresponding logical introduction rules *) (split_all_tac 1), (ftac lk_concl_ilc 1), (ftac lk_concl_irc 1), (clarsimp_tac (cesimps [in_single_count]) 1) ] ; val _ = qed_goal_spec_mp "cas_all" calk.thy "ALL X Y U V. (X |- mins A Y, mins A U |- V) : cas lkss A" (fn _ => [ EVERY casitacs, (fatac prstep_z 1 1), atac 6, (TRYALL (ares_tac [refl])), (simp_tac (esimps [symmetric mins_def]) 4), (asm_full_simp_tac (esimps [drs.all]) 1), (TRYALL (EVERY' [ (Simp_tac), (etac ball_match), (case_tac "x"), (asm_full_simp_tac (esimps [mins_def])) ] )) ]) ; (* simpler version of prstep goes with simpler rules (where principal formula not copied into conclusion) *) val sprstep' = prove_goal calk.thy "(ps, {#} |- {#A#}) : lkir & (qs, {#A#} |- {#}) : lkil & \ \ pse = map (extend (X |- Y)) ps & qse = map (extend (U |- V)) qs & \ \ set pse Un set qse <= derrec lkss {} & \ \ (ALL sfa X Y U V. (sfa, A) : ipsubfml --> \ \ ((X |- mins sfa Y), (mins sfa U |- V)) : cas lkss sfa) --> \ \ ((X |- mins A Y), (mins A U |- V)) : cas lkss A" (fn _ => [ Safe_tac, (etac lkil.elims 1), (ALLGOALS (etac lkir.elims)), (ALLGOALS (REPEAT o eresolve_tac ths)), (ALLGOALS (REPEAT o dtac (single_eq_single RS iffD1))), (ALLGOALS (eresolve_tac fc2Es' THEN' atac)), (* avoid the following until most subgoals removed *) Safe_tac, (ALLGOALS Full_simp_tac), Safe_tac, (ALLGOALS (rtac casI')), (TRYALL (EVERY' (tacips casD''))), (TRYALL (EVERY' (tacips casD3))) ]) RS mp ; val sprstep = meta_std (prove_goal calk.thy "?P --> ?s : car lkss A" (fn _ => [ (rtac impI 1), (rtac cas_car 1), (etac sprstep' 1), Safe_tac, (PRIMITIVE (fst o freeze_thaw o standard)), (REPEAT (EVERY' [ (rtac drs.derI), (REPEAT o (dresolve_tac lkne.intros)), (etac (lk_extI2 RS mem_same)), Simp_tac, (MSSG (REPEAT_ALL_NEW (resolve_tac [refl, conjI, extend_lem1, extend_lem2]))), (asm_full_simp_tac (esimps [drs.all]))] 1))])) ; val sprstep_z = full_simplify (esimps []) sprstep ; val _ = qed_goal_spec_mp "scas_all" calk.thy "ALL X Y U V. (X |- mins A Y, mins A U |- V) : cas lkss A" (fn _ => [ EVERY casitacs, (fatac sprstep_z 1 1), atac 4, (TRYALL (ares_tac [refl])), (simp_tac (esimps [symmetric mins_def]) 2), (asm_full_simp_tac (esimps [drs.all]) 1) ]) ;