--- 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 \<approx>"} @{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 \<approx>"} @{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))) \<approx> 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
--- 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 = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
abbreviation
- FUN_REL_syn (infixr "===>" 55)
+ FUN_REL_syn ("_ ===> _")
where
"E1 ===> E2 \<equiv> 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