structure tr = struct val thy = theory "tr" val ipt_mk_cases = InductivePackage.the_mk_cases thy ; end ; use_legacy_bindings tr.thy ; val _ = qed_goalw_spec_mp "wty_tyof" tr.thy [tyof_def] "(s :: 'a :: tr, ty) : wty --> tyof s = ty" (fn _ => [ (rtac impI 1), (rtac (tr_class.wty_unique RS sym) 1), atac 1, (etac someI 1) ]) ; val _ = qed_goal_spec_mp "snu_ty" tr.thy "(t, tya) : snu ty --> (t, tya) : wty" (fn _ => [ (induct_tac "ty" 1), Auto_tac]) ; val _ = qed_goal_spec_mp "snu_iff1" tr.thy "(t, tya) : snu ty --> (t, tya) : snu tya" (fn _ => [ (induct_tac "ty" 1), Auto_tac ]) ; val _ = qed_goalw_spec_mp "snu_iff2" tr.thy [Subty_def'] "(t, tya) : snu ty --> (tya, ty) : Subty" (fn _ => [ (induct_tac "ty" 1), (ALLGOALS Simp_tac), Safe_tac, (TRYALL (etac (nth (transitive_closure_trans, 5)))), Auto_tac ]) ; val _ = qed_goalw_spec_mp "snu_mono" tr.thy [Subty_def'] "x : snu tya --> (tya, ty) : Subty --> x : snu ty" (fn _ => [ (induct_tac "ty" 1), (fast_tac (ces [rtranclE]) 2), Clarify_tac 1, (etac rtranclE 1), Clarify_tac 1, (etac iSubty.elims 1), Auto_tac ]) ; val _ = qed_goalw "snu_iff" tr.thy [sn_d_def] "(t, tya) : snu ty = ((t, tya) : sn_d & (tya, ty) : Subty)" (fn _ => [ Safe_tac, Fast_tac 1, (etac snu_iff2 1), (dtac snu_iff1 1), (eatac snu_mono 1 1) ]) ; val _ = qed_goal "snl_iff" tr.thy "(t, tya) : snl ty = ((t, tya) : sn_d & (tya, ty) : pSubty)" (fn _ => [ (case_tac "ty" 1), (auto_tac (cesimps [snu_iff, pSubty_fun])) ]) ; val _ = qed_goal "snl_snu" tr.thy "snl ty <= snu ty" (fn _ => [ (case_tac "ty" 1), Auto_tac ]) ; val _ = qed_goalw "snu_iff3" tr.thy [redtd_def] "(t, tya) : snu ty = \ \ ((tya, ty) : Subty & t : wfp (redtd tya) & (t, tya) : wty)" (fn _ => [ (induct_tac "ty" 1), Force_tac 2, (force_tac (claset (), esimps [Subty_fun] delsimps [redstud.redstud_fun]) 1) ]) ; val _ = qed_goalw "sn_d_iff" tr.thy [sn_d_def] "(t, tya) : sn_d = (t : wfp (redtd tya) & (t, tya) : wty)" (fn _ => [ (rtac iffI 1), (clarify_tac (cds [snu_iff3 RS iffD1]) 1), (rtac UN_I 1), (auto_tac (cesimps [snu_iff3]))]) ; val _ = qed_goal "redstud_alt" tr.thy "redstud sn ty = (UN tya: {tya. (tya, ty) : Subty}. redstd sn tya) Un runul" (fn _ => [ (induct_tac "ty" 1), (simp_tac (esimps [Subty_def]) 2), (simp_tac (esimps [Subty_fun]) 1), Auto_tac]) ; (* results depending on axclass tr *) val _ = qed_goal_spec_mp "redstud_mono" tr.thy "(sn1 :: ('a :: tr * ctype) set) <= sn2 --> redstud sn1 ty <= redstud sn2 ty" (fn _ => [ (REPEAT (rtac impI 1)), (induct_tac "ty" 1), (TRYALL (dtac tr_class.redstd_mono)), Auto_tac ]) ; val _ = qed_goal_spec_mp "rd1c" tr.thy "redstd (snl ty) ty = redstd (sn_d :: ('a :: tr * ctype) set) ty" (fn _ => [ (rtac trans 1), (rtac sym 2), (rtac tr_class.rd1 2), (cong_tac 1), (rtac set_ext 1), (Clarsimp_tac 1), (rtac snl_iff 1) ]) ; val _ = qed_goal_spec_mp "rdu1" tr.thy "redstud sn ty = \ \ redstud (sn Int {(t :: 'a :: tr, tya). (tya, ty) : pSubty}) ty" (fn _ => [ (rtac equalityI 1), (rtac redstud_mono 2), Fast_tac 2, (induct_tac "ty" 1), (clarsimp_tac (cesimps [Un_upper2]) 2), (dtac (tr_class.rd1 RS equalityD1') 2), Full_simp_tac 2, (simp_tac (HOL_ss addsimps [redstud.redstud_fun]) 1), (REPEAT1 (rtac Un_mono 1)), (TRYALL (EVERY' [etac order_trans, rtac redstud_mono, (clarsimp_tac (cesimps [pSubty_fun, Subty_def]))])), (rtac equalityD1 1), (rtac tr_class.rd1 1), (TRYALL Fast_tac) ]) ; val _ = qed_goal_spec_mp "rdu1c" tr.thy "redstud (snl ty) ty = redstud (sn_d :: ('a :: tr * ctype) set) ty" (fn _ => [ (rtac trans 1), (rtac sym 2), (rtac rdu1 2), (cong_tac 1), (rtac set_ext 1), (Clarsimp_tac 1), (rtac snl_iff 1) ]) ; val _ = bind_thm ("redtd_def'", ([redtd_def RS def_imp_eq, rdu1c] MRS trans)) ; val _ = qed_goal_spec_mp "redtd_mono" tr.thy "(t', t) : redtd tya --> \ \ (tya, tyb) : Subty --> (t', t :: 'a :: tr) : redtd tyb" (fn _ => [ (rtac impI 1), (induct_tac "tyb" 1), (clarsimp_tac (cesimps [Subty_def]) 2), (simp_tac (esimps [Subty_fun]) 1), (auto_tac (cesimps [redtd_def'])) ]) ; val _ = qed_goal_spec_mp "redd_alt" tr.thy "redd = \ \ (UN tya: UNIV. redstd (sn_d :: ('a :: tr * ctype) set) tya) Un runul" (fn _ => [ (auto_tac (cesimps [redd_def, redtd_def', redstud_alt])) ]) ; val _ = bind_thm ("reddE", tacsthm [etac UnE 2, etac UN_E 2, etac thin_rl 2] (make_elim (redd_alt RS equalityD1'))) ; val _ = qed_goalw "runul_redd" tr.thy [redd_def, redtd_def] "runul <= redd" (fn _ => [ (fast_tac (cis [redstud.redstud_OTy RS equalityD2']) 1) ]) ; val runul_redd' = runul_redd RS subsetD ; val _ = bind_thm ("wfp_runul_redd", runul_redd RS wfp_mono RS subsetD) ; val _ = qed_goal_spec_mp "redstd_redd" tr.thy "p : redstd (sn_d :: ('a :: tr * ctype) set) ty --> p : redd" (fn _ => [ (auto_tac (cesimps [redd_alt])) ]) ; (* use redstd_tys, redd_tys for these val _ = qed_goal_spec_mp "redstd_Subty" tr.thy "(t', t :: 'a :: tr) : redstd sn ty --> (tyof t', tyof t) : Subty" (fn _ => [ Safe_tac, (dtac tr_class.redstd_tys 1), (clarify_tac (cds [wty_tyof]) 1) ]) ; val _ = qed_goal_spec_mp "redd_Subty" tr.thy "(t', t :: 'a :: tr) : redd --> (tyof t', tyof t) : Subty" (fn _ => [ Safe_tac, (clarsimp_tac (cesimps [redd_alt]) 1), Safe_tac, (etac redstd_Subty 1), (dtac tr_class.runul_tys 1), (safe_tac (cds [wty_tyof])), Asm_simp_tac 1]) ; *) val _ = qed_goal_spec_mp "redd_tys" tr.thy "(t, s :: 'a :: tr) : redd --> (EX tys tyt. \ \ (s, tys) : wty & (t, tyt) : wty & (tyt, tys) : Subty)" (fn _ => [ Safe_tac, (clarsimp_tac (cesimps [redd_alt]) 1), Safe_tac, (dtac tr_class.redstd_tys 1), (dtac tr_class.runul_tys 2), Auto_tac ]) ; val _ = qed_goal_spec_mp "run_rdu" tr.thy "runul <= redstud sn ty" (indAu "ty") ; val _ = qed_goal_spec_mp "ty_rdu'" tr.thy "(t', t :: 'a :: tr) : redtd tyb --> (t, ty) : wty --> (t', t) : redtd ty" (fn _ => [ (induct_tac "tyb" 1), (auto_tac (cesimps [redtd_def'])), (TRYALL (fatac (tr_class.redstd_tys RS conjunct1 RS tr_class.wty_unique) 1)), Auto_tac, (etac (run_rdu RS subsetD) 1) ]) ; val _ = qed_goalw_spec_mp "ty_rdu" tr.thy [redd_def] "(t', t :: 'a :: tr) : redd --> (t, ty) : wty --> (t', t) : redtd ty" (fn _ => [ (fast_tac (ces [ty_rdu']) 1) ]) ; val _ = qed_goal_spec_mp "wfp_rdu" tr.thy "(t :: 'a :: tr) : wfp (redtd tyr) --> (ALL ty. (t, ty) : wty --> \ \ (ty, tyr) : Subty --> t : wfp redd)" (fn _ => [ (rtac impI 1), (etac wfp.induct 1), (strip_tac 1), (rtac wfp.wfpI 1), (strip_tac 1), (fatac ty_rdu 1 1), (datac redtd_mono 1 1), (dtac redd_tys 1), Safe_tac, (datac tr_class.wty_unique 1 1), hyp_subst_tac 1, (datac sssy 1 1), Fast_tac 1]) ; val _ = qed_goal_spec_mp "wfp_redd_iff" tr.thy "(t :: 'a :: tr, ty) : wty --> (t : wfp redd) = (t : wfp (redtd ty))" (fn _ => [ Safe_tac, (etac wfp_rdu 2), (etac wfp_mono' 1), (rewtac redd_def), Auto_tac ]) ; val wfp_redd_iff' = rewrite_rule [redtd_def] wfp_redd_iff ; val _ = qed_goal_spec_mp "sn_d_wfp" tr.thy "(t :: 'a :: tr, ty) : sn_d = (t : wfp redd & (t, ty) : wty)" (fn _ => [ (simp_tac (esimps [sn_d_iff]) 1), Safe_tac, (TRYALL (fast_tac (cds [wfp_redd_iff]))) ]) ; val wfp_redd_wty' = prove_goal tr.thy "((EX ty. (t :: 'a :: tr, ty) : wty) --> t : wfp redd) --> t : wfp redd" (fn _ => [ (rtac impI 1), (rtac wfpI_alt 1), (strip_tac 1), (dtac redd_tys 1), Fast_tac 1 ]) ; val _ = bind_thm ("wfp_redd_wty", tacthm Safe_tac (wfp_redd_wty' RS mp)) ; val wfp_runul_wty' = prove_goal tr.thy "((EX ty. (t :: 'a :: tr, ty) : wty) --> t : wfp runul) --> t : wfp runul" (fn _ => [ (rtac impI 1), (rtac wfpI_alt 1), (strip_tac 1), (dtac tr_class.runul_tys 1), Fast_tac 1 ]) ; val _ = bind_thm ("wfp_runul_wty", tacthm Safe_tac (wfp_runul_wty' RS mp)) ; val _ = qed_goal_spec_mp "allrel_sn_d_wfp" tr.thy "ALL astys. ((As, astys) : allrel sn_d) = \ \ (set As <= wfp redd & (As :: 'a :: tr list, astys) : allrel wty)" (fn _ => [ (induct_tac "As" 1), (ALLGOALS Clarsimp_tac), (auto_tac (ces [allrelE1'], esimps [sn_d_wfp])) ]) ;