(* refers to paper Gore & Ramanayake, Valentini's Cut-Elimination for Provability Logic Resolved, as GR *) structure gltree = struct val thy = theory "gltree" end ; use_legacy_bindings gltree.thy ; val nz_or_nz = tacthm (TRYALL (etac not0_implies_Suc)) disj_forward ; val sum_Suc = prove_goal HOL_Gen.thy "m + n = Suc k --> m ~= 0 | n ~= 0" (fn _ => [ arith_tac 1 ]) RS mp ; val _ = qed_goal "del0s_append" gltree.thy "del0s B (V @ W) = del0s B V + del0s B W" (indAu "V") ; val _ = qed_goal_spec_mp "del0s_0_map" gltree.thy "(ALL p: set ps. del0 B (f p) = 0) --> del0s B (map f ps) = 0" (indAu "ps") ; val _ = qed_goal_spec_mp "del0s_0_iff" gltree.thy "(del0s B ps = 0) = (ALL p: set ps. del0 B p = 0)" (indAu "ps") ; val _ = qed_goal_spec_mp "del0s_same" gltree.thy "(ALL dt: set dts. del0 B (f dt) = del0 B dt) --> \ \ del0s B (map f dts) = del0s B dts" (indAu "dts") ; val _ = qed_goal_spec_mp "del0s_gt0" gltree.thy "del0s B dts > 0 --> (EX dt : set dts. del0 B dt > 0)" (indAu "dts") ; val () = bind_thm ("del0_extDT", prove_goal gltree.thy "(ALL x. del0 B (f x) = 0) --> (ALL x. conclDT (f x) = x) --> \ \ del0 B (extendDT f dt) = del0 B dt & \ \ del0s B (extendDTs f dts) = del0s B dts" (fn _ => [ (rtac impI 1), (rtac impI 1), (induct_tac "dt dts" 1), ALLGOALS Asm_simp_tac, (clarsimp_tac (cesimps [map_concl_extDT_same]) 1) ]) RS mp RS mp RS conjunct1) ; (* del0-preserving use of rules in glssnr *) val ext_del0p' = prove_goal gltree.thy "((ps, c) : derl glssnr --> (ALL dts. ps = map conclDT dts --> \ \ allDTs (frg (glsse S)) dts --> (EX dt. \ \ allDT (frg (glsse S)) dt & conclDT dt = c & \ \ premsDT dt = premsDTs dts & del0 B dt = del0s B dts))) & \ \ ((ps, cs) : dersl glssnr --> (ALL dts. ps = map conclDT dts --> \ \ allDTs (frg (glsse S)) dts --> \ \ (EX dtcs. allDTs (frg (glsse S)) dtcs & map conclDT dtcs = cs & \ \ premsDTs dtcs = premsDTs dts & del0s B dtcs = del0s B dts)))" (fn _ => [ (rtac drl.induct 1), Simp_tac 3, Force_tac 1, Clarify_tac 2, (dtac (sym RS map_appendD) 2), (clarsimp_tac (cesimps [allDTs_append]) 2), (REPEAT1 (EVERY [etac allE 2, etac impE 2, rtac refl 2])), mp_tac 2, mp_tac 2, Clarify_tac 2, (REPEAT_FIRST (resolve_tac [exI, conjI, refl])), Force_tac 2, (asm_simp_tac (esimps [premsDTs_append]) 2), (asm_simp_tac (esimps [del0s_append]) 2), (REPEAT (eresolve_tac [all_forward, imp_forward] 1)), Safe_tac, (res_inst_tac [("x", "Der concl dtcs")] exI 1), (clarsimp_tac (cesimps [allDTs, premsDTs]) 1), Safe_tac, (REPEAT1 (eatac not_glra_nr 1 1)), (etac (glsse_nr RS subsetD) 1) ]) ; val _ = bind_thm ("ext_del0pe", meta_std (ext_del0p' RS conjunct1)) ; val _ = bind_thm ("ext_del0p", mk_ss ext_del0pe) ; val getA' = prove_goal gltree.thy "(ALL n. del0 B dt = Suc n --> valid rls dt --> (EX dtA GB A GBA. \ \ GBA = (mset_map Box GB |- {#Box A#}) & premsDT dtA = [GBA] & \ \ conclDT dtA = conclDT dt & GBA : derrec rls {} & \ \ allDT (frg rls) dtA & del0 B dtA = n)) & \ \ (ALL n. del0s B dts = Suc n --> Ball (set dts) (valid rls) --> \ \ (EX dtAs GB A GBA. \ \ GBA = (mset_map Box GB |- {#Box A#}) & premsDTs dtAs = [GBA] & \ \ map conclDT dtAs = map conclDT dts & GBA : derrec rls {} & \ \ allDTs (frg rls) dtAs & del0s B dtAs = n))" (fn _ => [ (induct_tac "dt dts" 1), Simp_tac 2, Simp_tac 2, Clarsimp_tac 2, (ftac (sum_Suc RS nz_or_nz) 2), Safe_tac, (full_simp_tac (esimps [charf_def] addsplits [split_if_asm]) 1), (* bottom rule is glr *) (res_inst_tac [("x", "Unf a")] exI 1), (force_tac (ces [glra.elims, make_elim valid_derrec], esimps []) 1), (TRYALL (etac allE THEN' mp_tac)), (etac impE 1), (force_tac (ces [validUp], esimps []) 1), Safe_tac, (res_inst_tac [("x", "Der a dtAs")] exI 1), (res_inst_tac [("x", "dtA # list")] exI 2), (res_inst_tac [("x", "dertree # dtAs")] exI 3), (REPEAT_SOME (resolve_tac [exI, conjI])), (TRYALL atac), (ALLGOALS Asm_simp_tac), (TRYALL (clarsimp_tac (cesimps [valid_def, noPrems, allDTs]))) ]) ; val _ = bind_thm ("getA", meta_std (getA' RS conjunct1)) ; val del0s_update_lt = meta_std (prove_goal gltree.thy "ALL n. n < length xs --> del0 B dtA < del0 B (xs ! n) --> \ \ del0s B (xs[n := dtA]) < del0s B xs" (fn _ => [ (induct_tac "xs" 1), Simp_tac 1, (clarsimp_tac (claset (), esimps [] addsplits [nat.split]) 1) ]) ) ; val aec_tac = (REPEAT o (resolve_tac [exI, conjI]) THEN' atac) ; (* note - in this result A may equal B - if so, don't use the glr rule *) val _= qed_goal_spec_mp "glr_prem" gltree.thy "del0 B dt > 0 --> valid glss dt --> \ \ (EX p q A dtA. ([p], q) : glr A & Box B :# antec q & \ \ p : derrec glss {} & conclDT dtA = conclDT dt & premsDT dtA = [q] & \ \ allDT (frg glss) dtA & del0 B dtA < del0 B dt)" (fn _ => [ (res_inst_tac [("dertree", "dt")] dertree_induct 1), (Simp_tac 2), (Clarsimp_tac 1), Safe_tac, (dtac del0s_gt0 2), Clarify_tac 2, (datac bspec 1 2), mp_tac 2, (etac impE 2), (etac validUp 2), Simp_tac 2, (dtac (ex_nth RS iffD1) 2), Clarify_tac 2, (REPEAT (aec_tac 2)), (res_inst_tac [("x", "Der a (list[n:=dtA])")] exI 2), Safe_tac, (Simp_tac 2), (force_tac (cesimps [premsDTs, valid_def, concat_update]) 2), (clarsimp_tac (cesimps [allDTs, valid_def, map_update_eq]) 2), (dtac (set_update_subset_insert RS subsetD) 2), Fast_tac 2, Simp_tac 2, Safe_tac, (eatac del0s_update_lt 1 3), (clarsimp_tac (cesimps [map_update_eq]) 2), (thin_tac "Ball ?S ?P" 1), (etac (mk_dupE glra.elims) 1), (REPEAT_FIRST (resolve_tac [exI, conjI, conclDT_Unf, premsDT_Unf])), (asm_full_simp_tac init_ss 1), Asm_simp_tac 4, Simp_tac 3, (asm_full_simp_tac (esimps [charf_def] addsplits [split_if_asm]) 1), (ALLGOALS (asm_full_simp_tac (esimps [charf_def] addsplits [split_if_asm]))), Fast_tac 1, (dtac (validUp RS valid_derrec) 1), Auto_tac ]) ; (* val getA2 = prove_goal gltree.thy "dt = (mset_map Box X) |- {#Box B#}) --> del0 B dt = Suc n --> \ \ valid rls dt --> (EX dtA GB A GBA. \ \ AXB = (mins (Box A) (mset_map Box X) |- {#Box B#}) & premsDT dtA = [GBA] & \ \ GBA = (mset_map Box GB |- {#Box A#}) & premsDT dtA = [GBA] & \ \ conclDT dtA = conclDT dt & GBA : derrec rls {} & \ \ allDT (frg rls) dtA & del0 B dtA = n)) & \ *) val glss_gen_wk = [transfer gltree.thy glss_extrs_wk, le_plus1] MRS gen_wk_tree RS derl_dt ; val _ = qed_goal_spec_mp "glss_ext_wk" gltree.thy "allDT (frg glss) dt --> (EX dtw. conclDT dtw = conclDT dt + W & \ \ allDT (frg glss) dtw & premsDT dtw = premsDT dt)" (fn _ => [ (rtac impI 1), (cut_facts_tac [glss_gen_wk] 1), (Safe_tac), (rtac exI 1), (rtac conjI 1), (rtac trans 1), atac 2, (res_inst_tac [("f", "%x. if conclDT dt = x then dt else Unf x")] concl_extDT_same 1), Force_tac 1, (rtac conjI 1), (rtac (allDT_extDT RS iffD2) 1), Force_tac 1, Asm_simp_tac 1, (asm_simp_tac (esimps [prems_extDT]) 1) ]) ; (* adding weakening, contraction, onto the end of a tree, no change in del0 *) (* val wk_derl_glssnr = [wkrls_derl_iff RS iffD2, glssnr_extrs_wk] MRS drl_mono ; val wk_ext_del0 = zero_var_indexes (wk_derl_glssnr RS ext_del0p) ; val wk0 = read_instantiate [("dts", "[?dta]")] wk_ext_del0 ; val _ = bind_thm ("wk_del0", refl RSN (2, full_simplify (esimps []) wk0)) ; *) val wc_derl_glssnr' = wk_ctr_derl_iff RS iffD2 RS drl_mono ; val wc_derl_glssnr = tacsthm [ (rtac ([Un_subset_iff, conjI] MRS iffD2) 2), (rtac glssnr_extrs_wk 2), (rtac (ballI RS (UN_subset_iff RS iffD2)) 2), (rtac glssnr_extrs_ctr 2) ] wc_derl_glssnr' ; val wc_ext_del0 = zero_var_indexes (wc_derl_glssnr RS ext_del0p) ; val wc0 = read_instantiate [("dts", "[?dta]")] wc_ext_del0 ; val _ = bind_thm ("wc_del0", refl RSN (2, full_simplify (esimps []) wc0)) ; val _ = bind_thm ("wk_del0", seq_singles_mono RS wc_del0) ; val wk2 = read_instantiate [("dta", "Der ({#A#} |- {#A#}) []")] wk_del0 ; val _ = bind_thm ("ax_wk_del0", full_simplify (esimps []) wk2) ; val _ = qed_goal_spec_mp "map_eq_lem" List_thy "ALL xs. (ALL x: set xs. ALL y: set ys. f x = g y --> f' x = g' y) --> \ \ map f xs = map g ys --> map f' xs = map g' ys" (indAu "ys") ; val glr_tacs = [ (simp_tac (esimps [mset_map_union RS sym]) 1), (REPEAT_FIRST (resolve_tac [conjI, refl])), (simp_tac (esimps (mset_map_union :: union_ac)) 1) ] ; (* can add Box Y in antecedent, same width, a general theorem for extending by Box Y on the left, preserving del0 *) val _ = qed_goal_spec_mp "add_Box_ant" gltree.thy "~ (B :# Y) --> BoxY = mset_map Box Y --> allDT (frg glss) dt --> \ \ (EX dtY. conclDT dtY = conclDT dt + (BoxY |- 0) & \ \ premsDT dtY = map (extend (BoxY |- 0)) (premsDT dt) & \ \ allDT (frg glss) dtY & del0 B dtY = del0 B dt)" (fn _ => [ (rtac impI 1), (rtac impI 1), (res_inst_tac [("dertree", "dt")] dertree_induct 1), (REPEAT1 (resolve_tac [impI, exI, conjI, conclDT_Unf] 2)), (simp_tac (esimps [extend_def']) 2), Simp_tac 2, (rtac impI 1), (subgoal_tac "ALL dt:set list. ?P dt" 1), (etac ball_match 2), (etac mp 2), (eatac allDTD2 1 2), (thin_tac "Ball ?S ?P" 1), Clarsimp_tac 1, Safe_tac, (* rule is GLR *) etac glra.elims 1, Clarsimp_tac 1, (* level 16 *) (forw_inst_tac [("dt", "dtY"), ("W", "(Y|-0)")] glss_ext_wk 1), Clarify_tac 1, (res_inst_tac [("x", "Der ?c [dtw]")] exI 1), (REPEAT_FIRST (rtac conjI)), Simp_tac 1, Force_tac 1, Asm_simp_tac 1, (* last rule is glr *) (rtac (glr.I RS glss.glrI RS mem_same) 1), EVERY glr_tacs, (clarsimp_tac (cesimps [charf_def]) 1), (etac notE 1), (rtac (glra.I RS mem_same) 1), EVERY glr_tacs, (* level 29 *) (etac glss.elims 1), (fast_tac (cis [glr_a]) 3), (* last rule is axiom *) (cut_rules_tac [ax_wk_del0] 1), (etac ex_forward 1), Force_tac 1, Force_tac 1, (* last rule is extrs glne *) (dtac bchoice 1), (etac exE 1), (res_inst_tac [("x", "Der ?c (map f list)")] exI 1), Safe_tac, (ALLGOALS (simp_tac (esimps [premsDTs, map_concat]))), cong_tac 1, (asm_simp_tac (esimps [map_compose RS sym] addcongs [map_cong]) 1), (rtac conjI 1), (force_tac (cesimps [allDTs]) 2), (dres_inst_tac [("flr", "flr + (mset_map Box Y |- 0)")] glss.extI 1), (etac mem_same 1), (clarsimp_tac (cesimps ((map_compose RS sym) :: extend_def :: plus_ac)) 1), (rtac (map_eq_lem RS sym) 1), atac 2, (clarsimp_tac (cesimps (extend_def :: plus_ac)) 1), Safe_tac, (rtac del0s_same 2), (Force_tac 2), (subgoal_tac "(map conclDT list, a) : glssnr" 1), (dtac (in_extrs RS extrs_glra_not_nr) 1), (REPEAT (etac notE 1)), (etac extrs.I 1), (clarsimp_tac (cesimps [extend_def, map_compose RS sym]) 1), (rtac conjI 1), (rtac refl 2), (rtac (map_eq_lem RS sym) 1), atac 2, (clarsimp_tac (cesimps (extend_def :: plus_ac)) 1), (dtac glssnr.extI 1), Asm_full_simp_tac 1 ]) ; val add_Box_ant' = full_simplify (esimps []) add_Box_ant ; (* get the left branch of cut1 and cut2 in GR, Lemma 19 *) val _= qed_goal_spec_mp "glr_prem_ax_lem'" gltree.thy "B :# H --> (mset_map Box H |- {#Box A#}) = forget q --> \ \ premsDT dtq = [forget q] --> allDT (frg glss) dtq --> \ \ (EX dtA. conclDT dtA = ({#Box A#} |- 0) + conclDT dtq & \ \ valid glss dtA & del0 B dtA = del0 B dtq)" (fn _ => [ Clarify_tac 1, (case_tac "A = B" 1), (forw_inst_tac [("Y", "{#A#}")] ([thin_rl, refl] MRS add_Box_ant) 2), Asm_simp_tac 2, atac 2, Clarify_tac 2, (forw_inst_tac [("c", "({#Box A#} |- 0) + forget q")] (thin_rl RS ax_wk_del0) 2), (dtac sym 2), Force_tac 2, Clarify_tac 2, (res_inst_tac [("x", "extendDT (%p. if p = conclDT dt then dt else Unf p) dtY")] exI 2), (REPEAT_FIRST (rtac conjI)), (asm_simp_tac (esimps [concl_extDT_same]) 2), (asm_simp_tac (esimps [valid_def, allDT_extDT, prems_extDT, extend_def]) 2), (rtac trans 2), atac 3, (rtac del0_extDT 2), Force_tac 2, Force_tac 2, Safe_tac, (forw_inst_tac [("c", "forget q")] (thin_rl RS ax_wk_del0) 1), (dtac sym 1), (force_tac (cesimps [single_le]) 1), Clarify_tac 1, (forw_inst_tac [("B", "B"), ("dta", "extendDT (%p. if p = conclDT dt then dt else Unf p) dtq")] (thin_rl RS wk_del0) 1), (asm_simp_tac (esimps [allDT_extDT, extend_def]) 2), (etac ex_forward 2), Safe_tac, (asm_simp_tac (esimps [valid_def, allDT_extDT, prems_extDT, extend_def]) 2), (asm_simp_tac (esimps [concl_extDT_same]) 1), (asm_simp_tac (esimps [valid_def, allDT_extDT, prems_extDT, extend_def]) 1), (Asm_simp_tac 1), (stac del0_extDT 1), Auto_tac ]) ; (* alternative to last bit above (res_inst_tac [("x", "extlistDT [dta] dtA")] exI 1), (REPEAT_FIRST (rtac conjI)), (asm_simp_tac (esimps [concl_extlDT_same]) 1), (asm_simp_tac (esimps [valid_def, allDT_extlDT, prems_extlDT, extend_def]) 1), not using this, working with extlistDT seems more difficult, haven't done the extlistDT counterpart of del0_extDT *) val glr_prem_ax_lem'' = (refl RSN (2, rewrite_rule [forget_def] glr_prem_ax_lem')) ; val _= qed_goal_spec_mp "glr_prem_ax_lem" gltree.thy "([p], q) : glr A --> Box B :# antec q --> \ \ conclDT dtq = f dt --> premsDT dtq = [q] --> \ \ allDT (frg glss) dtq --> del0 B dtq < ddt --> \ \ (EX dtA. conclDT dtA = ({#Box A#} |- 0) + f dt & \ \ valid glss dtA & del0 B dtA < ddt)" (fn _ => [ Clarify_tac 1, (etac glr.elims 1), Clarsimp_tac 1, (datac glr_prem_ax_lem'' 2 1), (etac ex_forward 1), Asm_simp_tac 1 ]) ; val _= qed_goal_spec_mp "glr_prem_ax" gltree.thy "del0 B dt > 0 --> valid glss dt --> \ \ (EX A dtA. conclDT dtA = ({#Box A#} |- 0) + conclDT dt & \ \ valid glss dtA & del0 B dtA < del0 B dt)" (fn _ => [ Clarify_tac 1, (datac glr_prem 1 1), Clarify_tac 1, (dtac glr_prem_ax_lem 1), TRYALL atac, etac exI 1 ]) ; val ms_ss = (esimps [mset_map_union, Box_mset_map_delete, count_ms_delete] addsplits [split_if_asm]) ; val ms_css = (cis [singles_mono], ms_ss) ; (** Lemma 19 of GR - descriptions refer to Lemma 19 **) val ewc = zero_var_indexes ([le_plus1, validD1] MRS wk_del0) ; val singles_insert_leI = singles_insert_le RS transfer MS.thy order_trans ; (* gr19a - first part, get \Lambda_{11} and \Lambda_{12}, using cut1 & cut2 *) val _ = qed_goal_spec_mp "gr19a" gltree.thy "([conclDT dtglp], seq) : glrxb X B --> \ \ valid glss dtglp --> del0 B dtglp = Suc n --> muxbn B n --> \ \ (EX A H dtH. ({#Box A#} + mset_map Box X + X |- {#B#}) : derrec glss {} \ \ & ({#Box A#} + mset_map Box (X + ms_delete {B} H) + H |- {#A#}) \ \ : derrec glss {} & \ \ premsDT dtH = [mset_map Box H |- {#Box A#}] & \ \ conclDT dtH = conclDT dtglp & allDT (frg glss) dtH & del0 B dtH <= n)" (fn _ => [ (safe_tac (ces [glrxb.elims])), (* dtglp is right branch of cut1 and cut4 *) (cut_rules_tac [glr_prem] 1), (etac xt1 2), (rtac zero_less_Suc 2), atac 2, Clarify_tac 1, (ftac glr_prem_ax_lem 1), TRYALL atac, Clarsimp_tac 1, (rename_tac "dtaxbu" 1), (* need to weaken dtaxbu with (A |- 0) and apply glr *) (forw_inst_tac [("B", "B"), ("dta", "dtaxbu"), ("n", "{#A#} |- 0")] (thin_rl RS ewc) 1), atac 1, Clarify_tac 1, (rename_tac "dtaxbw" 1), (subgoal_tac "([conclDT dtaxbw], \ \ (mset_map Box X + {#Box A#} |- {#Box B#})) : glr B" 1), (cut_inst_tac [("X", "mins A X"), ("B", "B")] glr.I 2), (etac mem_same 2), (force_tac (cesimps ([mins_def, mset_map_union] @ plus_ac)) 2), (* prepare to eliminate cut1 and cut2 *) (subgoal_tac "ALL dtb. \ \ (Der (mset_map Box X + {#Box A#} |- {#Box B#}) [dtaxbw], dtb) \ \ : masdt glss (Box B)" 1), (force_tac (cesimps (muxbn_def :: le_simps)) 2), (* eliminate cut1 *) (eres_inst_tac [("x", "dtglp")] all_dupE 1), (safe_tac (ces [masdt.elims, mar.elims])), (force_tac (ces [glss.glrI], esimps [valid_def]) 1), (clarsimp_tac (cesimps [ms_delete_sum]) 1), (* get conclusion of \Lambda_{11} *) (res_inst_tac [("x", "A")] exI 1), (rtac conjI 1), (chop_last (etac wc_glss 1)), (simp_tac (esimps [set_of_delete]) 1), (safe_tac (cis [singles_mono, singles_insert_leI])), (* now get \Lambda_{12} *) (dres_inst_tac [("a", "p")] derrec_valid 1), Clarify_tac 1, (rename_tac "dtgap" 1), (* dtgap, with conclusion p, is right branch of cut2 *) (eres_inst_tac [("x", "dtgap")] allE 1), (safe_tac (ces [masdt.elims, mar.elims])), (force_tac (ces [glss.glrI], esimps [valid_def]) 1), (etac glr.elims 1), Clarsimp_tac 1, (* level 36 *) (* q is Box Xa |- Box A, ie, Xa is H + Bn of the proof *) (res_inst_tac [("x", "Xa")] exI 1), (rtac conjI 1), (chop_last (etac wc_glss 1)), (clarsimp_tac (cesimps [set_of_delete, mset_map_union]) 1), (safe_tac (cis [singles_mono])), (force_tac ms_css 1), Force_tac 1 ]) ; val _ = qed_goal_spec_mp "gr19b" gltree.thy "([conclDT dtglp], seq) : glrxb X B --> valid glss dtglp --> \ \ del0 B dtglp = Suc n --> mas glss B = UNIV --> muxbn B n --> \ \ (EX dtn. valid glss dtn & conclDT dtn = conclDT dtglp & del0 B dtn <= n)" (fn _ => [ Safe_tac, (case_tac "B :# X" 1), (* simple case where B is in X *) (clarify_tac (ces [glrxb.elims]) 1), (forw_inst_tac [("B", "B"), ("A", "B")] (thin_rl RS ax_wk_del0) 1), (etac ex_forward 2), (force_tac (cesimps [valid_def]) 2), (force_tac (cesimps [single_le]) 1), (fatac gr19a 3 1), (clarify_tac (ces [glrxb.elims]) 1), (* now for cut3 *) (etac (UNIV_I RSN (2, equalityD2') RS masE_pair) 1), (etac impE 1), (eatac conjI 1 1), (clarsimp_tac (cesimps [mar_eq, ms_delete_sum, mset_map_union]) 1), (subgoal_tac "(mset_map Box (X + ms_delete {B} H) + (X + ms_delete {B} H) \ \ + {#Box A#} |- {#A#}) : derrec glss {}" 1), (chop_last (etac wc_glss 2)), (simp_tac (esimps [set_of_delete]) 2), (safe_tac (cis [singles_mono])), (TRYALL (clarsimp_tac ms_css o incr)), (* get tree (del0 doesn't matter), then apply glr rule *) (chop_last (dtac derrec_valid 1)), (REPEAT (thin_tac ("?s : derrec glss {}") 1)), (Clarify_tac 1), (subgoal_tac "([conclDT dt], ?cg) : glr A" 1), (Clarsimp_tac 2), (rtac glr.I 2), (* add this use of glr rule to the tree, and weaken *) (subgoal_tac "EX dtg. valid glss dtg & del0 B dtg = 0 & \ \ conclDT dtg = (mset_map Box (X + H) |- {#Box A#})" 1), (forw_inst_tac [("dta", "Der ?dc [dt]")] (thin_rl RS wk_del0) 2), (Clarsimp_tac 3), (etac ([glr.I RS glss.glrI, validD1] MRS transfer gltree.thy conjI) 3), (etac ex_forward 3), Safe_tac, atac 5, (etac trans 4), (force_tac (cesimps [valid_def]) 3), (force_tac (cesimps [mset_map_union, mset_map_mono]) 2), (Simp_tac 2), Safe_tac, (fast_tac (cis [glr_a]) 3), (clarsimp_tac (cesimps [count_ms_delete, charf_def]) 2), (* now dtg is \Lambda_3, conclusion Box (X + H) |- Box A, del0 = 0 *) (* now take dtH, and add Box X to its antecedent, result is dtY *) (datac (refl RSN (2, add_Box_ant')) 1 1), Clarsimp_tac 1, (* do the contraction of Box X at bottom of dtY, result is dtaa *) (forw_inst_tac [("dta", "dtY"), ("c", "(mset_map Box X + X + {#Box B#} |- {#B#})"), ("B", "B")] (thin_rl RS wc_del0) 1), atac 2, (force_tac ms_css 1), (* now put this together with dtg *) Clarify_tac 1, (rename_tac "dtgp" 1), (res_inst_tac [("x", "extendDT (%p. if p = conclDT dtg then dtg else Unf p) dtgp")] exI 1), (REPEAT_FIRST (rtac conjI)), (asm_full_simp_tac (esimps [mset_map_union, valid_def, allDT_extDT, prems_extDT, extend_def]) 1), (asm_simp_tac (esimps [concl_extDT_same]) 1), (rtac xt4 1), (rtac (del0_extDT RS sym) 2), Auto_tac ]) ; val _ = qed_goal_spec_mp "gr19c'" gltree.thy "muxbn B n --> mas glss B = UNIV --> muxbn B (Suc n)" (fn _ => [ (Clarify_tac 1), (simp_tac (esimps [muxbn_def]) 1), (Clarify_tac 1), (case_tac "del0 B dtp = Suc n" 1), (force_tac (cesimps [muxbn_def]) 2), (rtac masdt.I 1), (Clarify_tac 1), (etac glr_xbE 1), (ftac gr19b 1), (TRYALL atac), (etac validUpD 1), Force_tac 1, (Clarify_tac 1), (rewtac muxbn_def), (REPEAT_SOME (eresolve_tac [allE, impE, asm_rl])), Asm_simp_tac 1, (etac glr_xbI 1), (dtac masdtD 1), Asm_full_simp_tac 3, atac 2, (clarsimp_tac (cesimps [valid_def]) 1) ]) ; val _ = qed_goal_spec_mp "gr19c" gltree.thy "muxbn B 0 --> mas glss B = UNIV --> muxbn B n" (fn _ => [ (Clarify_tac 1), (induct_tac "n" 1), atac 1, (eatac gr19c' 1 1) ]) ; (* this is, in effect, Lemma 19 where width > 0 *) val _ = qed_goal_spec_mp "gr19d" gltree.thy "([conclDT dtglp], seq) : glrxb X B --> valid glss dtglp --> \ \ mas glss B = UNIV --> muxbn B 0 --> \ \ (mset_map Box X + X |- {#B#}) : derrec glss {}" (fn _ => [ Safe_tac, (ftac glr_xbI 1), (safe_tac (ces [glrxb.elims])), (datac gr19c 1 1), (rewtac muxbn_def), (eres_inst_tac [("xa", "dtglp")] allE3 1), mp_tac 1, (etac impE 1), (rtac order_refl 1), (safe_tac (ces [masdt.elims, mar.elims])), (force_tac (cis [glss.glrI], esimps [valid_def]) 1), (Clarsimp_tac 1), (etac wc_glss 1), (simp_tac (esimps [set_of_delete]) 1), (safe_tac (cis [singles_mono])) ]) ; val _ = qed_goal_spec_mp "derrec_del0" gltree.thy "(c : derrec (extrs glne) (snd ` (idrls Un glre {B}) Int derrec glss{}))-->\ \ (EX dt. valid glss dt & del0 B dt = 0 & conclDT dt = c)" (fn _ => [ Safe_tac, (etac drs.inductr 1), Safe_tac, (res_inst_tac [("x", "Der b []")] exI 1), (simp_tac (esimps [valid_def]) 1), (etac idrls.elims 1), Fast_tac 1, (etac glre.elims 1), Asm_full_simp_tac 1, (dtac (transfer gltree.thy inv_glr RS derrec_valid) 1), (etac exE 1), (res_inst_tac [("x", "Der b [dt]")] exI 1), (clarsimp_tac (cesimps [valid_def, charf_def]) 1), (dtac bchoice 1), Clarify_tac 1, (res_inst_tac [("x", "Der concl (map f ps)")] exI 1), (subgoal_tac "map conclDT (map f ps) = ps" 1), (asm_simp_tac (esimps [map_compose RS sym] addcongs [map_cong]) 2), (ftac extrs_ne_not_glra 1), (clarsimp_tac (cesimps [valid_def, charf_def, premsDTs, allDTs, del0s_0_map]) 1), (etac (mk_mono' glss_extrs) 1) ]) ; val _ = qed_goal_spec_mp "del0_derrec" gltree.thy "valid glss dt --> del0 B dt = 0 --> (conclDT dt : \ \ derrec (extrs glne) (snd ` (idrls Un glre {B}) Int derrec glss {}))" (fn _ => [ (res_inst_tac [("dertree", "dt")] dertree_induct 1), Simp_tac 2, Safe_tac, (full_simp_tac (esimps [] addsplits [split_if_asm]) 1), (clarsimp_tac (cesimps [valid_def]) 2), (dtac (glss_alt RS equalityD1') 2), Safe_tac, (* case last rule in extrs glne *) (etac drs.derI' 3), (Clarsimp_tac 3), (datac bspec 1 3), (etac impE 3), (etac mp 4), (clarsimp_tac (cesimps [allDTs, premsDTs]) 3), (clarsimp_tac (cesimps [del0s_0_iff]) 3), (* case last rule in idrls *) (rtac drs.dpI 2), (rtac IntI 2), (rtac image_eqI 2), (etac UnI1 3), Force_tac 2, (rtac drs.derI' 2), (etac idrls.elims 2), Clarsimp_tac 2, (rtac glss.axiom 2), Force_tac 2, (* case last rule in glra *) (rtac drs.dpI 1), (rtac IntI 1), (dtac valid_derrec 2), Force_tac 2, (rtac image_eqI 1), (rtac UnI2 2), (etac glra.elims 2), (rtac mem_same 2), etac sym 3, Force_tac 1, (rtac glre.I 1), (clarsimp_tac (claset (), esimps [charf_def] addsplits [split_if_asm]) 1) ]) ; val _ = qed_goal "del0_iff_derrec" gltree.thy "(EX dt. valid glss dt & del0 B dt = 0 & conclDT dt = c) = \ \ (c : derrec (extrs glne) (snd ` (idrls Un glre {B}) Int derrec glss {}))" (fn _ => [ (safe_tac (cis [del0_derrec, derrec_del0])) ]) ; val _ = qed_goal_spec_mp "glr_dt_lem" gltree.thy "valid glss dtp --> ([conclDT dtp], seq) : glrxb X B --> seq : derrec glss {}" (fn _ => [ Safe_tac, (dtac valid_derrec 1), (eatac (glss_glrxbI RS drs.derIsingle) 1 1) ]) ; val _ = qed_goal_spec_mp "gr19e'" gltree.thy "valid glss dtp --> del0 B dtp = 0 --> \ \ conclDT dtp = (mset_map Box X + X + {#Box B#} |- {#B#}) --> \ \ (mset_map Box X + X |- {#B#}) : derrec glss {}" (fn _ => [ Safe_tac, (ftac glr_dt_lem 1), Force_tac 1, (dres_inst_tac [("Us", "{#B#}"), ("Vs", "mset_map Box X")] (del0_derrec RS bbbcf_ps_lem) 1), atac 1, (clarsimp_tac (cesimps [bbbcf_def, etr_def, ms_delete_sum]) 1), (rtac (order_refl RS derrec_trans RS wc_glss) 1), (chop_tac 1 (etac der_mono 1)), (Clarsimp_tac 3), (rtac singles_mono 3), Simp_tac 4, Safe_tac, (TRYALL (dtac in_set_of_ms_delete THEN' Fast_tac)), (etac (mk_mono' glsse_glss) 1), (* identity rule *) (etac idrls.elims 1), (clarsimp_tac (cesimps [etr_def]) 1), (case_tac "A = Box B" 1), Force_tac 1, (clarsimp_tac (cesimps [ms_delete_notin]) 1), (rtac (id_adm_glss RS id_admD) 1), ALLGOALS Simp_tac, (* GLR rule, Box B not in antecedent *) (etac glre.elims 1), (clarsimp_tac (cesimps [etr_def, ms_delete_notin]) 1), (chop_tac 1 (etac (wk_adm_glss RS wk_admD_alt) 1)), Simp_tac 1 ]) ; val _ = qed_goal_spec_mp "gr19e" gltree.thy "valid glss dtp --> del0 B dtp = 0 --> ([conclDT dtp], seq) : glrxb X B --> \ \ (mset_map Box X + X |- {#B#}) : derrec glss {}" (fn _ => [ Safe_tac, (etac glrxb.elims 1), Clarify_tac 1, (eatac gr19e' 2 1) ]) ; (* gr19d and gr19e together give GR, Lemma 19 *) val _ = qed_goalw_spec_mp "bbbc_glr_w0" gltree.thy [gsfg_def, bblblf_def] "valid glss dtp --> del0 B dtp = 0 --> mas glss B = UNIV --> \ \ ([conclDT dtp], seq) : glrxb X B --> (ps, c) : glra --> \ \ gsfg glss drls (bblblf {#B#} X) A (ps, c)" (fn _ => [ (clarsimp_tac (ces [glra.elims], esimps [gen_step.simps, etr_def]) 1), (datac gr19e 2 1), (etac (UNIV_I RSN (2, equalityD2') RS masE_pair) 1), (etac impE 1), (chop_tac 1 (etac conjI 1)), atac 1, (REPEAT (thin_tac "?p : derrec ?rls {}" 1)), dtac marD 1, (* now weaken and use the glr rule *) (rtac (glss_glraI RS drs.derIsingle) 1), (REPEAT (etac thin_rl 1)), (rtac (glra.I RS mem_same) 1) , (simp_tac (esimps [mset_map_union RS sym, Box_mset_map_delete1 RS sym]) 1), (REPEAT_FIRST (resolve_tac [conjI, refl])), (etac wc_glss 1), Simp_tac 1, (safe_tac (cis [singles_mono])), (clarsimp_tac (cesimps [mset_map_union]) 1), (clarsimp_tac (cesimps [ms_delete_sum, Box_mset_map_delete1, mset_map_union]) 1), Safe_tac, (ALLGOALS (asm_full_simp_tac (esimps [count_ms_delete] addsplits [split_if_asm]))) ]) ; val _ = qed_goal_spec_mp "bbbc_glr_w0_all" gltree.thy "valid glss dtp --> del0 B dtp = 0 --> mas glss B = UNIV --> \ \ ([conclDT dtp], seq) : glrxb X B --> (ps, c) : glss --> \ \ gsfg glss drls (bblblf {#B#} X) A (ps, c)" (fn _ => [ (safe_tac (ces [glss_altE])), (eatac bbbc_glr_w0 4 3), (* last rule is axiom *) (etac idrls.elims 1), (clarsimp_tac (cesimps [bblbl_bc]) 1), (rtac bbbc_ax_lemg 1), (datac glr_dt_lem 1 1), (etac glrxb.elims 1), Force_tac 1, (rtac id_adm_glss 1), (* last rule is in extrs glne *) (etac extrs_singleE 1), (simp_tac (esimps [glss_e]) 1), (eatac bblbl_glne_lemge 1 1) ]) ; val cg0thm = zero_var_indexes ([gsfg_def RS def_imp_eq RS fun_cong, bbbc_glr_w0_all] MRS iffD1) ; val cw0 = zero_var_indexes (tacsthm [(rtac cg0thm 1), atac 5, TRYALL (etac thin_rl), prune_params_tac] gslem1) ; val _ = bind_thm ("del0_ca", tacthm prune_params_tac (read_instantiate [("dtp", "%x a b. ?dt"), ("seq", "%x a b. ?sq")] cw0)) ; val del0_ca' = rewrite_rule [bblblf_def, etr_def] del0_ca ; val caB_muxbn' = prove_goalw gltree.thy [muxbn_def] "mas glss B = UNIV --> muxbn B 0" (fn _ => [ (safe_tac (cis [masdt.I] addSEs [glr.elims])), (dtac validUpD 1), Force_tac 1, (datac del0_ca 2 1), Asm_simp_tac 1, (rtac glrxb.I 1), (etac valid_derrec 1), (case_tac "conclDT dtb" 1), (clarsimp_tac (cesimps [mar_eq, bblblf_def, etr_def]) 1) ]) RS mp ; val _ = qed_goal_spec_mp "caB_muxbn" gltree.thy "mas glss B = UNIV --> muxbn B n" (fn _ => [ rtac impI 1, (rtac (caB_muxbn' RS gr19c) 1), TRYALL atac ]) ; val _ = bind_thm ("cut_glr", order_refl RSN (3, ObjectLogic.rulify (rewrite_rule [muxbn_def] caB_muxbn))) ;