# HG changeset patch # User Cezary Kaliszyk # Date 1255600653 -7200 # Node ID 3134acbcc42c612ded1a407c83be66eac45cb6d5 # Parent 41a2ab50dd890ba6cadf3963ca876819aaff969f# Parent 9d41f680d755c81a6a427fb7fdbad8cb99609a07 Merged diff -r 9d41f680d755 -r 3134acbcc42c QuotMain.thy --- a/QuotMain.thy Thu Oct 15 11:53:11 2009 +0200 +++ b/QuotMain.thy Thu Oct 15 11:57:33 2009 +0200 @@ -774,31 +774,6 @@ ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *} ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *} -(* Has all the theorems about fset plugged in. These should be parameters to the tactic *) -ML {* - fun transconv_fset_tac' ctxt = - REPEAT_ALL_NEW (FIRST' [ - rtac @{thm list_eq_refl}, - rtac @{thm cons_preserves}, - rtac @{thm mem_respects}, - 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} - ]) -*} - -ML {* - val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1})) - val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs - val cgoal = cterm_of @{theory} goal - val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) -*} - -(*notation ( output) "prop" ("#_" [1000] 1000) *) -notation ( output) "Trueprop" ("#_" [1000] 1000) - lemma atomize_eqv[atomize]: shows "(Trueprop A \ Trueprop B) \ (A \ B)" proof @@ -819,10 +794,36 @@ then show "A \ B" by (rule eq_reflection) qed +(* 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 mem_respects}, + 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_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs + val cgoal = cterm_of @{theory} goal + val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) +*} + +(*notation ( output) "prop" ("#_" [1000] 1000) *) +notation ( output) "Trueprop" ("#_" [1000] 1000) + + prove {* (Thm.term_of cgoal2) *} - apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) - apply (atomize(full)) - apply (tactic {* transconv_fset_tac' @{context} 1 *}) + apply (tactic {* transconv_fset_tac' @{context} *}) done thm length_append (* Not true but worth checking that the goal is correct *) @@ -833,9 +834,7 @@ val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) *} prove {* Thm.term_of cgoal2 *} - apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) - apply (atomize(full)) - apply (tactic {* transconv_fset_tac' @{context} 1 *}) + apply (tactic {* transconv_fset_tac' @{context} *}) sorry thm m2 @@ -846,9 +845,7 @@ val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) *} prove {* Thm.term_of cgoal2 *} - apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) - apply (atomize(full)) - apply (tactic {* transconv_fset_tac' @{context} 1 *}) + apply (tactic {* transconv_fset_tac' @{context} *}) done thm list_eq.intros(4) @@ -862,9 +859,7 @@ (* It is the same, but we need a name for it. *) prove zzz : {* Thm.term_of cgoal3 *} - apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) - apply (atomize(full)) - apply (tactic {* transconv_fset_tac' @{context} 1 *}) + apply (tactic {* transconv_fset_tac' @{context} *}) done lemma zzz' : @@ -874,25 +869,15 @@ 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) ML {* val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)})) val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs -*} -ML {* - val cgoal = - Toplevel.program (fn () => - cterm_of @{theory} goal - ) -*} -ML {* + 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 {* LocalDefs.unfold_tac @{context} fset_defs *} ) - apply (atomize(full)) - apply (tactic {* transconv_fset_tac' @{context} 1 *}) + apply (tactic {* transconv_fset_tac' @{context} *}) done section {* handling quantifiers - regularize *} @@ -1042,9 +1027,6 @@ cterm_of @{theory} (regularise @{term "All (P :: trm \ bool)"} @{typ "trm"} @{term "RR"} @{context}); *} - - - ML {* fun atomize_thm thm = let @@ -1062,9 +1044,6 @@ trm == new_trm *) - - - ML {* val li = Thm.freezeT (atomize_thm @{thm list.induct}) *} prove {* @@ -1076,10 +1055,7 @@ apply (rule RIGHT_RES_FORALL_REGULAR) prefer 2 apply (assumption) - apply (rule allI) - apply (rule impI) - apply (rule impI) - apply (assumption) + apply (metis) done ML {* val li = Thm.freezeT (atomize_thm @{thm card1_suc}) *} @@ -1088,11 +1064,9 @@ Logic.mk_implies ((prop_of li), (regularise (prop_of li) @{typ "'a List.list"} @{term "op \"} @{context})) *} - apply (simp only: equiv_res_forall[OF equiv_list_eq]) - apply (simp only: equiv_res_exists[OF equiv_list_eq]) + apply (simp add: equiv_res_forall[OF equiv_list_eq] equiv_res_exists[OF equiv_list_eq]) done -thm card1_suc ML {* @{thm card1_suc_r} OF [li] *} ML {* val li = Thm.freezeT (atomize_thm @{thm fold1.simps(2)}) *}