# HG changeset patch # User Cezary Kaliszyk # Date 1256385618 -7200 # Node ID 7cf227756e2a2fdc2982db715c241f65e0968f51 # Parent da38ce2711a607d74b145c60b916cc968d37dce5 Finally completely lift the previously lifted theorems + clean some old stuff diff -r da38ce2711a6 -r 7cf227756e2a FSet.thy --- a/FSet.thy Sat Oct 24 13:00:54 2009 +0200 +++ b/FSet.thy Sat Oct 24 14:00:18 2009 +0200 @@ -277,14 +277,13 @@ fun regularize thm rty rel rel_eqv lthy = let val g = build_regularize_goal thm rty rel lthy; - val tac = - atac ORELSE' (simp_tac ((Simplifier.context lthy HOL_ss) addsimps + fun tac ctxt = + (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps [(@{thm equiv_res_forall} OF [rel_eqv]), (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW - ((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' - (RANGE [fn _ => all_tac, atac]) THEN' (MetisTools.metis_tac lthy [])); - val cgoal = cterm_of (ProofContext.theory_of lthy) g; - val cthm = Goal.prove_internal [] cgoal (fn _ => tac 1); + (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac])) ORELSE' + (MetisTools.metis_tac ctxt [])); + val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1); in cthm OF [thm] end @@ -438,8 +437,6 @@ apply (tactic {* rtac thm 1 *}) done -thm list.recs(2) - thm m2 ML {* atomize_thm @{thm m2} *} @@ -555,9 +552,12 @@ ML {* ObjectLogic.rulify qthm *} thm fold1.simps(2) - +thm list.recs(2) -ML {* val ind_r_a = atomize_thm @{thm fold1.simps(2)} *} +ML {* val ind_r_a = atomize_thm @{thm m2} *} + (* prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \"} @{context} *} + apply (simp add: equiv_res_forall[OF equiv_list_eq] equiv_res_exists[OF equiv_list_eq]) done *) + ML {* val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \"} @{thm equiv_list_eq} @{context} *} ML {* val rt = build_repabs_term @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} @@ -565,7 +565,7 @@ *} (*prove rg apply(atomize(full)) -apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})*) +apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})*) ML {* val (g, thm, othm) = Toplevel.program (fn () => repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} @@ -614,95 +614,11 @@ ML {* lift @{thm m1} *} ML {* lift @{thm list_eq.intros(4)} *} ML {* lift @{thm list_eq.intros(5)} *} - -(* Has all the theorems about fset plugged in. These should be parameters to the tactic *) -ML {* - fun transconv_fset_tac' ctxt = - (LocalDefs.unfold_tac @{context} fset_defs) THEN - ObjectLogic.full_atomize_tac 1 THEN - REPEAT_ALL_NEW (FIRST' [ - rtac @{thm list_eq_refl}, - rtac @{thm cons_preserves}, - rtac @{thm memb_rsp}, - rtac @{thm card1_rsp}, - rtac @{thm QUOT_TYPE_I_fset.R_trans2}, - CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})), - Cong_Tac.cong_tac @{thm cong}, - rtac @{thm ext} - ]) 1 -*} - -ML {* - val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1})) - val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} - val cgoal = cterm_of @{theory} goal - val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) -*} +(* ML {* lift @{thm length_append} *} *) (*notation ( output) "prop" ("#_" [1000] 1000) *) notation ( output) "Trueprop" ("#_" [1000] 1000) - -prove {* (Thm.term_of cgoal2) *} - apply (tactic {* transconv_fset_tac' @{context} *}) - done - -thm length_append (* Not true but worth checking that the goal is correct *) -ML {* - val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm length_append})) - val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} - val cgoal = cterm_of @{theory} goal - val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) -*} -prove {* Thm.term_of cgoal2 *} - apply (tactic {* transconv_fset_tac' @{context} *}) - sorry - -thm m2 -ML {* - val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2})) - val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} - val cgoal = cterm_of @{theory} goal - val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) -*} -prove {* Thm.term_of cgoal2 *} - apply (tactic {* transconv_fset_tac' @{context} *}) - done - -thm list_eq.intros(4) -ML {* - val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)})) - val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} - val cgoal = cterm_of @{theory} goal - val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) - val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2) -*} - -(* It is the same, but we need a name for it. *) -prove zzz : {* Thm.term_of cgoal3 *} - apply (tactic {* transconv_fset_tac' @{context} *}) - done - -(*lemma zzz' : - "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \ REP_fset (INSERT a (ABS_fset xs)))" - using list_eq.intros(4) by (simp only: zzz) - -thm QUOT_TYPE_I_fset.REPS_same -ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *} -*) - -thm list_eq.intros(5) -(* prove {* build_repabs_goal @{context} (atomize_thm @{thm list_eq.intros(5)}) consts @{typ "'a list"} @{typ "'a fset"} *} *) -ML {* - val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)})) - val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} - val cgoal = cterm_of @{theory} goal - val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) -*} -prove {* Thm.term_of cgoal2 *} - apply (tactic {* transconv_fset_tac' @{context} *}) - done - ML {* fun lift_theorem_fset_aux thm lthy = let diff -r da38ce2711a6 -r 7cf227756e2a QuotScript.thy --- a/QuotScript.thy Sat Oct 24 13:00:54 2009 +0200 +++ b/QuotScript.thy Sat Oct 24 14:00:18 2009 +0200 @@ -127,7 +127,7 @@ "FUN_REL E1 E2 f g = (\x y. E1 x y \ E2 (f x) (g y))" abbreviation - FUN_REL_syn (infixr "===>" 55) + FUN_REL_syn ("_ ===> _") where "E1 ===> E2 \ FUN_REL E1 E2" @@ -509,7 +509,6 @@ shows "!f. Ex f = Bex (Respects R) ((absf ---> id) f)" sorry -(* Currently fixed, should be general *) lemma ho_all_prs: "op = ===> op = ===> op = All All" apply (auto) done