val g = goal SN2.thy ; val gw = goalw SN2.thy ; open SN2 ; context SN2.thy ; val th = snHered_def RS meta_eq_to_obj_eq RS iffD1 RS mp ; val () = qed_goalw_spec_mp "sn_snH" SN2.thy [snHered_def] "dt : sn_set --> snHered dt" (fn _ => [Auto_tac]) ; val () = qed_goal_spec_mp "hereds_sn" SN2.thy "(ALL dts. isSubt dt dts --> snHered dts) = (dt : sn_set)" (fn _ => [ rtac iffI 1, etac rev_mp 1, (res_inst_tac [("dertree1", "dt")] dertree_induct 1), Simp_tac 2, rtac impI 1, etac all_dupE 1, etac impE 1, rtac isSubt_refl 1, etac th 1, Simp_tac 1, rtac subsetI 1, (datac bspec 1 1), etac mp 1, etac all_match 1, Safe_tac, etac notE 1, (eatac (isSubtI RS isSubt_trans) 1 1), (rtac sn_snH 1), (eatac subt_sn 1 1)]) ; val hereds_sn' = hereds_sn RS iffD1 ; (* alternative proofs of hereds_sn' *) val hereds_sn' = prove_goalw SN2.thy [snHered_def] "(ALL dts. isSubt dt dts --> snHered dts) --> dt : sn_set" (fn _ => [ (rtac impI 1), (forw_inst_tac [("a", "dt"), ("P", "%x. isSubt dt x --> x : sn_set"), ("r", "{(y,x). y : set (nextUp x)}")] (thin_rl RS wf_induct) 1), Clarsimp_tac 2, (safe_tac (claset () addSafter ("", etac allE THEN' mp_tac))), (dtac isSubt_trans 2), (etac nextUpSubt 2), contr_tac 2, (rtac wf_nextUp 1) ]) RS mp ; val hereds_sn' = prove_goalw SN2.thy [snHered_def] "(ALL dts. isSubt dt dts --> snHered dts) --> dt : sn_set" (fn _ => [ (rtac impI 1), (rtac (wfp_nextUp RS wfp_hereds_sn) 1), (clarsimp_tac (cesimps [isSubt_rtc_nextUp]) 1), Fast_tac 1]) RS mp ; fun tacsf _ = [case_tac "dt" 1, Asm_simp_tac 2, Asm_simp_tac 1, Safe_tac, etac (defn45bsn RS iffD2) 1, Fast_tac 1] ; val () = qed_goalw_spec_mp "notCutHered'" SN2.thy [snHered_def] "~ isCut dt --> snHered dt" tacsf ; val () = qed_goalw_spec_mp "notCutHered" SN2.thy [snHered_def] "botRule dt ~= cutr --> snHered dt" tacsf ; val () = qed_goal_spec_mp "bothRedP" SN2.thy "cutReduces dt dtn --> isSubt dtn dts --> isCut dts --> \ \ isSubt dt dts & dt ~= dts | (dts, dt) : cutorder" (fn _ => [(case_tac "dt" 1), (ALLGOALS (asm_simp_tac (esimps [c8redP_def]))), (safe_tac (set_cs delrules [disjCI])), (ALLGOALS (EVERY' [etac allE, etac impE, etac conjI])), (etac cut_bot 1), atac 2, (ALLGOALS (EVERY' [etac disjE, etac disjI1, rtac disjI2])), (rewrite_goals_tac [inv_image_def, measure_def, cutorder_def, lex_prod_def]), (ALLGOALS Asm_simp_tac), (TRYALL (fast_tac (ces [ipsubfml_size])))]) ; val () = qed_goalw_spec_mp "dth" SN2.thy [snHered_def, subset_def] "(ALL dt'. (dt', dt) : dtorder --> snHered dt') --> snHered dt" (fn _ => [Safe_tac, rtac sn_set.snI 1, strip_tac 1, (case_tac "dtn" 1), (case_tac "dt" 1), (ALLGOALS Asm_full_simp_tac), (etac ro_elim 1), (* case of reduction of proper subtree *) (ftac sn1red_allsn 1), Fast_tac 1, (dtac snOnered 1), Fast_tac 1, etac allE 1, etac impE 1, etac mp 2, Force_tac 2, Asm_simp_tac 1, eresolve_tac (sn1order.intrs RL dtorder.intrs) 1, (* level 17 *) (* cut-reduction of whole tree *) rtac hereds_sn' 1, Safe_tac, (ftac cutReduces_IsCut 1), (rtac (excluded_middle RS disjE) 1), etac notCutHered' 1, (datac bothRedP 2 1), Safe_tac, (* dts is proper subtree of original *) dtac not_sym 1, (asm_full_simp_tac (esimps [isSub1t]) 1), (etac bexE 1), (datac bspec 1 1), (datac subt_sn 1 1), etac sn_snH 1, (* dts is cutorder-smaller than original *) (etac allE 1), (etac impE 1), (etac dtorder.dtc 1), (asm_simp_tac (esimps [snHered_def, subset_def]) 1)]) ; (* every derivation tree is snHered *) val () = qed_goal "all_snH" SN2.thy "snHered dt" (fn _ => [cut_facts_tac [wf_dtorder] 1, rewtac wf_def, (eres_inst_tac [("x", "snHered")] allE 1), etac impE 1, Safe_tac, etac dth 1, Auto_tac]) ; (* every derivation tree is sn *) val () = qed_goalw "all_sn" SN2.thy [strongNorm_def] "strongNorm dt" (fn _ => [rtac hereds_sn' 1, Safe_tac, rtac all_snH 1]) ; (* alternative proof *) val ss = simpset () delsimps [funpow_Suc] ; val wfp_nured2 = prove_goal SN2.thy "{dt. set (nextUp dt) <= sn_set} <= wfp nured" (fn _ => [Safe_tac, rtac ccontr 1, (dres_inst_tac [("s", "sn1order")] dth_lemg 1), (cut_facts_tac [wf_sn1order] 1), (asm_full_simp_tac (esimps [wf_wfp]) 1), Safe_tac, (datac sn1_sn 1 1), (case_tac "ptc" 1), (case_tac "ptr" 1), (ALLGOALS (eresolve_tac ron.elims)), (ALLGOALS Asm_full_simp_tac), (datac sn1red_allsn 1 1), (dtac sn1order.sn1I 1), contr_tac 1]) ; val () = bind_thm ("wfp_nured", [wfp_nured1, wfp_nured2] MRS equalityI) ; val () = qed_goal "wfp_nured'" SN2.thy "dt : wfp nured = (set (nextUp dt) <= sn_set)" (fn _ => [(simp_tac (esimps [wfp_nured]) 1)]) ; val ss = simpset () delsimps [funpow_Suc] ; val () = qed_goal_spec_mp "nured_sn" SN2.thy "(ptr, pt) : nured --> set (nextUp pt) <= sn_set --> \ \ set (nextUp ptr) <= sn_set & (ptr, pt) : sn1order" (fn _ => [(rtac impI 1), eresolve_tac reduction_onered_nured.elims 1, Safe_tac, (dtac snOnered 1), (dtac (sn1red_allsn RS hd sn1order.intrs) 3), Auto_tac]) ; val () = qed_goal_spec_mp "nuredtc_sn" SN2.thy "(ptr, pt) : nured^+ --> set (nextUp pt) <= sn_set --> \ \ set (nextUp ptr) <= sn_set & (ptr, pt) : sn1order^+" (fn _ => [rtac impI 1, (etac trancl_induct 1), (rtac impI 1), (datac nured_sn 1 1), Fast_tac 1, (rtac impI 1), (datac nured_sn 1 1), Safe_tac, (eatac (trancl_into_rtrancl RS rtrancl_into_trancl1) 1 1)]) ; val () = qed_goal_spec_mp "dth1_lem" SN2.thy "pt ~: sn_set --> set (nextUp pt) <= sn_set --> \ \ (EX ptr ptc. (ptr, pt) : sn1order^* & cutReduces ptr ptc & ptc ~: sn_set)" (fn _ => [ (strip_tac 1), (ftac (dth_lemg RSN (2, thin_rl)) 1), (full_simp_tac (esimps [sn_set_def]) 1), (full_simp_tac (esimps [wfp_nured' RS sym]) 1), (Safe_tac), (subgoal_tac "cutReduces ptr ptc" 1), (rtac exI 1), (rtac exI 1), (Safe_tac), atac 2, ((etac reduction_onered_nured.elim THEN_ALL_NEW Asm_full_simp_tac) 3), (asm_full_simp_tac (esimps [sn_set_def]) 2), (full_simp_tac (HOL_ss addsimps [reflcl_trancl RS sym]) 1), Safe_tac, (datac nuredtc_sn 1 1), Safe_tac]) ; val () = qed_goal_spec_mp "dth1" SN2.thy "(ALL dt'. (dt', dt) : cutorder --> snHered dt') --> snHered dt" (fn _ => [ rtac impI 1, (simp_tac (esimps [snHered_def]) 1), Safe_tac, rtac ccontr 1, (datac dth1_lem 1 1), Safe_tac, etac notE 1, (fatac sn1_sn 1 1), (* ptr cutReduces to ptc, need to show ptc is sn *) rtac hereds_sn' 1, strip_tac 1, (case_tac "ptr" 1), Asm_full_simp_tac 2, hyp_subst_tac 1, (* show any subtree dts of ptc is snHered *) (ftac cutReduces_IsCut 1), (rtac (excluded_middle RS disjE) 1), etac notCutHered' 1, (* dts has cut at the bottom *) (datac bothRedP 2 1), Safe_tac, (* dts is proper subtree of ptr *) dtac not_sym 1, (asm_full_simp_tac (esimps [isSub1t]) 1), (etac bexE 1), (datac subsetD 1 1), (* dts is subtree of dta, which is in nextUp ptr *) (datac subt_sn 1 1), etac sn_snH 1, (* dts is cutorder-smaller than ptr, and therefore then dt *) (etac allE 1), (etac mp 1), (eatac sntr'' 1 1)]) ; (* every derivation tree is snHered, as also proved above *) val () = qed_goal "all_snH1" SN2.thy "snHered dt" (fn _ => [cut_facts_tac [wf_cutorder] 1, rewtac wf_def, (eres_inst_tac [("x", "snHered")] allE 1), etac impE 1, Safe_tac, etac dth1 1, Auto_tac]) ; (* every derivation tree is sn *) val () = qed_goalw "all_sn1" SN2.thy [strongNorm_def] "strongNorm dt" (fn _ => [rtac hereds_sn' 1, Safe_tac, rtac all_snH1 1]) ;