--- a/Quot/Examples/FSet.thy Tue Dec 08 11:17:56 2009 +0100
+++ b/Quot/Examples/FSet.thy Tue Dec 08 11:20:01 2009 +0100
@@ -303,7 +303,7 @@
lemma "IN x EMPTY = False"
apply(tactic {* procedure_tac @{context} @{thm m1} 1 *})
apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} 1 *})
apply(tactic {* clean_tac @{context} 1*})
done
@@ -331,8 +331,6 @@
apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
done
-ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
-
lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
done
@@ -348,7 +346,7 @@
apply(tactic {* regularize_tac @{context} 1 *})
defer
apply(tactic {* clean_tac @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1*})+
+apply(tactic {* inj_repabs_tac @{context} 1*})+
done
lemma list_induct_part:
@@ -390,10 +388,6 @@
where
"INSERT2 \<equiv> op #"
-ML {* val quot = @{thms Quotient_fset Quotient_fset2} *}
-ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
-ML {* fun lift_tac_fset lthy t = lift_tac lthy t *}
-
lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
done
@@ -425,9 +419,6 @@
apply (auto)
sorry
-ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}
-ML {* fun lift_tac_fset lthy t = lift_tac lthy t *}
-
lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"
apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *})
done
--- a/Quot/Examples/IntEx.thy Tue Dec 08 11:17:56 2009 +0100
+++ b/Quot/Examples/IntEx.thy Tue Dec 08 11:20:01 2009 +0100
@@ -136,15 +136,6 @@
shows "(intrel ===> intrel ===> intrel) my_plus my_plus"
by (simp)
-ML {* val qty = @{typ "my_int"} *}
-ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
-ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *}
-
-ML {* fun lift_tac_intex lthy t = lift_tac lthy t *}
-
-ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
-ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [rel_refl] [trans2] *}
-
lemma test1: "my_plus a b = my_plus a b"
apply(rule refl)
done
@@ -152,7 +143,7 @@
lemma "PLUS a b = PLUS a b"
apply(tactic {* procedure_tac @{context} @{thm test1} 1 *})
apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
apply(tactic {* clean_tac @{context} 1 *})
done
@@ -168,7 +159,7 @@
apply(rule ballI)
apply(rule apply_rsp[OF Quotient_my_int plus_rsp])
apply(simp only: in_respects)
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
apply(tactic {* clean_tac @{context} 1 *})
done
@@ -180,7 +171,7 @@
apply(tactic {* procedure_tac @{context} @{thm test3} 1 *})
apply(rule impI)
apply(rule plus_rsp)
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
apply(tactic {* clean_tac @{context} 1 *})
done
@@ -188,7 +179,7 @@
lemma "PLUS a b = PLUS b a"
apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
apply(tactic {* clean_tac @{context} 1 *})
done
@@ -203,7 +194,7 @@
lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"
apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
apply(tactic {* clean_tac @{context} 1 *})
done
@@ -214,7 +205,7 @@
lemma "foldl PLUS x [] = x"
apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})
apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
apply(tactic {* clean_tac @{context} 1 *})
apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])
done
@@ -225,7 +216,7 @@
lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)"
apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *})
apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
apply(tactic {* clean_tac @{context} 1 *})
apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] cons_prs[OF Quotient_my_int])
done
@@ -236,7 +227,7 @@
lemma "foldl f (x::my_int) ([]::my_int list) = x"
apply(tactic {* procedure_tac @{context} @{thm ho_tst3} 1 *})
apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
(* TODO: does not work when this is added *)
(* apply(tactic {* lambda_prs_tac @{context} 1 *})*)
apply(tactic {* clean_tac @{context} 1 *})
@@ -249,7 +240,7 @@
lemma "(\<lambda>x. (x, x)) (y::my_int) = (y, y)"
apply(tactic {* procedure_tac @{context} @{thm lam_tst} 1 *})
apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
apply(tactic {* clean_tac @{context} 1 *})
apply(simp add: pair_prs)
done
@@ -325,7 +316,7 @@
lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"
apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *})
defer
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
apply(tactic {* clean_tac @{context} 1 *})
apply(subst babs_rsp)
apply(tactic {* clean_tac @{context} 1 *})
@@ -343,7 +334,7 @@
lemma "(\<lambda>(y :: my_int => my_int). y) = (\<lambda>(x :: my_int => my_int). x)"
apply(tactic {* procedure_tac @{context} @{thm lam_tst3b} 1 *})
defer
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
apply(tactic {* clean_tac @{context} 1 *})
apply(subst babs_rsp)
apply(tactic {* clean_tac @{context} 1 *})
--- a/Quot/Examples/IntEx2.thy Tue Dec 08 11:17:56 2009 +0100
+++ b/Quot/Examples/IntEx2.thy Tue Dec 08 11:20:01 2009 +0100
@@ -166,10 +166,6 @@
text{*The integers form a @{text comm_ring_1}*}
-ML {* val qty = @{typ "int"} *}
-ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
-ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "int" *}
-
instance int :: comm_ring_1
proof
fix i j k :: int
--- a/Quot/Examples/LFex.thy Tue Dec 08 11:17:56 2009 +0100
+++ b/Quot/Examples/LFex.thy Tue Dec 08 11:20:01 2009 +0100
@@ -218,12 +218,6 @@
thm akind_aty_atrm.induct
thm kind_ty_trm.induct
-ML {*
- val quot = @{thms Quotient_KIND Quotient_TY Quotient_TRM}
- val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) @{thms alpha_equivps}
- val reps_same = map (fn x => @{thm Quotient_rel_rep} OF [x]) quot
- val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quot
-*}
lemma
assumes a0:
@@ -261,7 +255,7 @@
apply -
apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} 1 *})
apply(fold perm_kind_def perm_ty_def perm_trm_def)
apply(tactic {* clean_tac @{context} 1 *})
(*
--- a/Quot/Examples/LamEx.thy Tue Dec 08 11:17:56 2009 +0100
+++ b/Quot/Examples/LamEx.thy Tue Dec 08 11:20:01 2009 +0100
@@ -169,54 +169,48 @@
apply (simp_all add: rlam.inject alpha_refl)
done
-ML {* val qty = @{typ "lam"} *}
-ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} *}
-
-ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
-ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *}
-ML {* fun lift_tac_lam lthy t = lift_tac lthy t *}
lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)"
-apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *})
+apply (tactic {* lift_tac @{context} @{thm pi_var_com} 1 *})
done
lemma pi_app: "(pi\<Colon>('x \<times> 'x) list) \<bullet> App (x\<Colon>lam) (xa\<Colon>lam) = App (pi \<bullet> x) (pi \<bullet> xa)"
-apply (tactic {* lift_tac_lam @{context} @{thm pi_app_com} 1 *})
+apply (tactic {* lift_tac @{context} @{thm pi_app_com} 1 *})
done
lemma pi_lam: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Lam (a\<Colon>name) (x\<Colon>lam) = Lam (pi \<bullet> a) (pi \<bullet> x)"
-apply (tactic {* lift_tac_lam @{context} @{thm pi_lam_com} 1 *})
+apply (tactic {* lift_tac @{context} @{thm pi_lam_com} 1 *})
done
lemma fv_var: "fv (Var (a\<Colon>name)) = {a}"
-apply (tactic {* lift_tac_lam @{context} @{thm rfv_var} 1 *})
+apply (tactic {* lift_tac @{context} @{thm rfv_var} 1 *})
done
lemma fv_app: "fv (App (x\<Colon>lam) (xa\<Colon>lam)) = fv x \<union> fv xa"
-apply (tactic {* lift_tac_lam @{context} @{thm rfv_app} 1 *})
+apply (tactic {* lift_tac @{context} @{thm rfv_app} 1 *})
done
lemma fv_lam: "fv (Lam (a\<Colon>name) (x\<Colon>lam)) = fv x - {a}"
-apply (tactic {* lift_tac_lam @{context} @{thm rfv_lam} 1 *})
+apply (tactic {* lift_tac @{context} @{thm rfv_lam} 1 *})
done
lemma a1: "(a\<Colon>name) = (b\<Colon>name) \<Longrightarrow> Var a = Var b"
-apply (tactic {* lift_tac_lam @{context} @{thm a1} 1 *})
+apply (tactic {* lift_tac @{context} @{thm a1} 1 *})
done
lemma a2: "\<lbrakk>(x\<Colon>lam) = (xa\<Colon>lam); (xb\<Colon>lam) = (xc\<Colon>lam)\<rbrakk> \<Longrightarrow> App x xb = App xa xc"
-apply (tactic {* lift_tac_lam @{context} @{thm a2} 1 *})
+apply (tactic {* lift_tac @{context} @{thm a2} 1 *})
done
lemma a3: "\<lbrakk>(x\<Colon>lam) = [(a\<Colon>name, b\<Colon>name)] \<bullet> (xa\<Colon>lam); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> Lam a x = Lam b xa"
-apply (tactic {* lift_tac_lam @{context} @{thm a3} 1 *})
+apply (tactic {* lift_tac @{context} @{thm a3} 1 *})
done
lemma alpha_cases: "\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P;
\<And>x xa xb xc. \<lbrakk>a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P;
\<And>x a b xa. \<lbrakk>a1 = Lam a x; a2 = Lam b xa; x = [(a, b)] \<bullet> xa; a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> P\<rbrakk>
\<Longrightarrow> P"
-apply (tactic {* lift_tac_lam @{context} @{thm alpha.cases} 1 *})
+apply (tactic {* lift_tac @{context} @{thm alpha.cases} 1 *})
done
lemma alpha_induct: "\<lbrakk>(qx\<Colon>lam) = (qxa\<Colon>lam); \<And>(a\<Colon>name) b\<Colon>name. a = b \<Longrightarrow> (qxb\<Colon>lam \<Rightarrow> lam \<Rightarrow> bool) (Var a) (Var b);
@@ -224,16 +218,16 @@
\<And>(x\<Colon>lam) (a\<Colon>name) (b\<Colon>name) xa\<Colon>lam.
\<lbrakk>x = [(a, b)] \<bullet> xa; qxb x ([(a, b)] \<bullet> xa); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> qxb (Lam a x) (Lam b xa)\<rbrakk>
\<Longrightarrow> qxb qx qxa"
-apply (tactic {* lift_tac_lam @{context} @{thm alpha.induct} 1 *})
+apply (tactic {* lift_tac @{context} @{thm alpha.induct} 1 *})
done
lemma var_inject: "(Var a = Var b) = (a = b)"
-apply (tactic {* lift_tac_lam @{context} @{thm rvar_inject} 1 *})
+apply (tactic {* lift_tac @{context} @{thm rvar_inject} 1 *})
done
lemma lam_induct:" \<lbrakk>\<And>name. P (Var name); \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2);
\<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk> \<Longrightarrow> P lam"
-apply (tactic {* lift_tac_lam @{context} @{thm rlam.induct} 1 *})
+apply (tactic {* lift_tac @{context} @{thm rlam.induct} 1 *})
done
lemma var_supp:
--- a/Quot/QuotMain.thy Tue Dec 08 11:17:56 2009 +0100
+++ b/Quot/QuotMain.thy Tue Dec 08 11:20:01 2009 +0100
@@ -144,11 +144,10 @@
declare [[map * = (prod_fun, prod_rel)]]
declare [[map "fun" = (fun_map, fun_rel)]]
-(* FIXME: This should throw an exception:
-declare [[map "option" = (bla, blu)]]
-*)
-(* identity quotient is not here as it has to be applied first *)
+(* Throws now an exception: *)
+(* declare [[map "option" = (bla, blu)]] *)
+
lemmas [quotient_thm] =
fun_quotient prod_quotient
@@ -160,22 +159,17 @@
lemmas [quotient_equiv] =
identity_equivp prod_equivp
-ML {* maps_lookup @{theory} "*" *}
-ML {* maps_lookup @{theory} "fun" *}
-
-
(* definition of the quotient types *)
(* FIXME: should be called quotient_typ.ML *)
use "quotient.ML"
-
(* lifting of constants *)
use "quotient_def.ML"
section {* Simset setup *}
-(* since HOL_basic_ss is too "big", we need to set up *)
-(* our own minimal simpset *)
+(* Since HOL_basic_ss is too "big" for us, *)
+(* we set up our own minimal simpset. *)
ML {*
fun mk_minimal_ss ctxt =
Simplifier.context ctxt empty_ss
@@ -184,11 +178,10 @@
*}
ML {*
-(* TODO/FIXME not needed anymore? *)
-fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
+fun OF1 thm1 thm2 = thm2 RS thm1
*}
-section {* atomize *}
+section {* Atomize Infrastructure *}
lemma atomize_eqv[atomize]:
shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
@@ -220,24 +213,20 @@
end
*}
-section {* infrastructure about id *}
+section {* Infrastructure about id *}
+
+print_attributes
(* TODO: think where should this be *)
lemma prod_fun_id: "prod_fun id id \<equiv> id"
by (rule eq_reflection) (simp add: prod_fun_def)
-(* FIXME: make it a list and add map_id to it *)
-lemmas id_simps =
+lemmas [id_simps] =
fun_map_id[THEN eq_reflection]
id_apply[THEN eq_reflection]
id_def[THEN eq_reflection,symmetric]
prod_fun_id
-ML {*
-fun simp_ids thm =
- MetaSimplifier.rewrite_rule @{thms id_simps} thm
-*}
-
section {* Debugging infrastructure for testing tactics *}
ML {*
@@ -265,7 +254,7 @@
fun NDT ctxt s tac thm = tac thm
*}
-section {* Matching of terms and types *}
+section {* Matching of Terms and Types *}
ML {*
fun matches_typ (ty, ty') =
@@ -278,9 +267,7 @@
then (List.all matches_typ (tys ~~ tys'))
else false
| _ => false
-*}
-ML {*
fun matches_term (trm, trm') =
case (trm, trm') of
(_, Var _) => true
@@ -292,37 +279,7 @@
| _ => false
*}
-section {* Infrastructure for collecting theorems for starting the lifting *}
-
-ML {*
-fun lookup_quot_data lthy qty =
- let
- val qty_name = fst (dest_Type qty)
- val SOME quotdata = quotdata_lookup lthy qty_name
- (* TODO: Should no longer be needed *)
- val rty = Logic.unvarifyT (#rtyp quotdata)
- val rel = #rel quotdata
- val rel_eqv = #equiv_thm quotdata
- val rel_refl = @{thm equivp_reflp} OF [rel_eqv]
- in
- (rty, rel, rel_refl, rel_eqv)
- end
-*}
-
-ML {*
-fun lookup_quot_thms lthy qty_name =
- let
- val thy = ProofContext.theory_of lthy;
- val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2")
- val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same")
- val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10")
- val quot = PureThy.get_thm thy ("Quotient_" ^ qty_name)
- in
- (trans2, reps_same, absrep, quot)
- end
-*}
-
-section {* Regularization *}
+section {* Computation of the Regularize Goal *}
(*
Regularizing an rtrm means:
@@ -489,13 +446,13 @@
raise (LIFT_MATCH "regularize (default)")
*}
+section {* Regularize Tactic *}
+
ML {*
fun equiv_tac ctxt =
(K (print_tac "equiv tac")) THEN'
REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt))
-*}
-ML {*
fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
*}
@@ -537,7 +494,7 @@
SOME thm2
end
handle _ => NONE
-(* FIXME/TODO: what is the place where the exception can be raised: matching_prs? *)
+(* FIXME/TODO: what is the place where the exception is raised: matching_prs? *)
*}
ML {*
@@ -560,20 +517,23 @@
shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
by (simp add: equivp_reflp)
-(* FIXME/TODO: How does regularizing work? *)
-(* FIXME/TODO: needs to be adapted
-To prove that the raw theorem implies the regularised one,
-we try in order:
+(* Regularize Tactic *)
- - Reflexivity of the relation
- - Assumption
- - Elimnating quantifiers on both sides of toplevel implication
- - Simplifying implications on both sides of toplevel implication
- - Ball (Respects ?E) ?P = All ?P
- - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
+(* 0. preliminary simplification step according to *)
+thm ball_reg_eqv bex_reg_eqv babs_reg_eqv (* the latter of no use *)
+ ball_reg_eqv_range bex_reg_eqv_range
+(* 1. eliminating simple Ball/Bex instances*)
+thm ball_reg_right bex_reg_left
+(* 2. monos *)
+(* 3. commutation rules for ball and bex *)
+thm ball_all_comm bex_ex_comm
+(* 4. then rel-equality (which need to be instantiated to avoid loops *)
+thm eq_imp_rel
+(* 5. then simplification like 0 *)
+(* finally jump back to 1 *)
-*)
+
ML {*
fun regularize_tac ctxt =
let
@@ -586,24 +546,19 @@
addsimprocs [simproc] addSolver equiv_solver
(* TODO: Make sure that there are no list_rel, pair_rel etc involved *)
(* can this cause loops in equiv_tac ? *)
- val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt)
+ val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt)
in
simp_tac simpset THEN'
REPEAT_ALL_NEW (CHANGED o FIRST' [
- rtac @{thm ball_reg_right},
- rtac @{thm bex_reg_left},
+ resolve_tac @{thms ball_reg_right bex_reg_left},
resolve_tac (Inductive.get_monos ctxt),
- rtac @{thm ball_all_comm},
- rtac @{thm bex_ex_comm},
+ resolve_tac @{thms ball_all_comm bex_ex_comm},
resolve_tac eq_eqvs,
- (* should be equivalent to the above, but causes loops: *)
- (* rtac @{thm eq_imp_rel} THEN' SOLVES' (equiv_tac ctxt), *)
- (* the culprit is aslread rtac @{thm eq_imp_rel} *)
simp_tac simpset])
end
*}
-section {* Injections of rep and abses *}
+section {* Calculation of the Injected Goal *}
(*
Injecting repabs means:
@@ -658,8 +613,7 @@
val yvar = Free (y, T)
val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s'))
in
- if rty = qty
- then result
+ if rty = qty then result
else mk_repabs lthy (rty, qty) result
end
@@ -667,8 +621,7 @@
(inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s'))
| (Free (_, T), Free (_, T')) =>
- if T = T'
- then rtrm
+ if T = T' then rtrm
else mk_repabs lthy (T, T') rtrm
| (_, Const (@{const_name "op ="}, _)) => rtrm
@@ -678,35 +631,33 @@
let
val rty = fastype_of rtrm
in
- if rty = T'
- then rtrm
+ if rty = T' then rtrm
else mk_repabs lthy (rty, T') rtrm
end
| _ => raise (LIFT_MATCH "injection")
*}
-section {* RepAbs Injection Tactic *}
+section {* Injection Tactic *}
ML {*
fun quotient_tac ctxt =
REPEAT_ALL_NEW (FIRST'
[rtac @{thm identity_quotient},
resolve_tac (quotient_rules_get ctxt)])
-*}
-(* solver for the simplifier *)
-ML {*
fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
*}
ML {*
fun solve_quotient_assums ctxt thm =
- let val gl = hd (Drule.strip_imp_prems (cprop_of thm)) in
- thm OF [Goal.prove_internal [] gl (fn _ => quotient_tac ctxt 1)]
- end
- handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing"
+let
+ val goal = hd (Drule.strip_imp_prems (cprop_of thm))
+in
+ thm OF [Goal.prove_internal [] goal (fn _ => quotient_tac ctxt 1)]
+end
+handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing"
*}
(* Not used *)
@@ -914,9 +865,9 @@
(* reflexivity of operators arising from Cong_tac *)
| Const (@{const_name "op ="},_) $ _ $ _
- => rtac @{thm refl} ORELSE'
+ => rtac @{thm refl} (*ORELSE'
(resolve_tac trans2 THEN' RANGE [
- quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])
+ quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])*)
(* TODO: These patterns should should be somehow combined and generalized... *)
| (Const (@{const_name fun_rel}, _) $ _ $ _) $
@@ -943,32 +894,49 @@
*}
ML {*
-fun inj_repabs_tac ctxt rel_refl trans2 =
+fun inj_repabs_step_tac ctxt rel_refl trans2 =
(FIRST' [
- inj_repabs_tac_match ctxt trans2,
+ NDT ctxt "0" (inj_repabs_tac_match ctxt trans2),
(* R (t $ \<dots>) (t' $ \<dots>) ----> apply_rsp provided type of t needs lifting *)
+
NDT ctxt "A" (apply_rsp_tac ctxt THEN'
- (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
+ RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)]),
+
+ (* TODO/FIXME: I had to move this after the apply_rsp_tac - is this right *)
+ NDT ctxt "B" (resolve_tac trans2 THEN'
+ RANGE [quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]),
+
(* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *)
(* merge with previous tactic *)
- NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN'
+ NDT ctxt "C" (Cong_Tac.cong_tac @{thm cong} THEN'
(RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
+
(* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
- NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam),
+ NDT ctxt "D" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam),
+
(* resolving with R x y assumptions *)
NDT ctxt "E" (atac),
+
(* reflexivity of the basic relations *)
(* R \<dots> \<dots> *)
- NDT ctxt "D" (resolve_tac rel_refl)
+ NDT ctxt "F" (resolve_tac rel_refl)
])
*}
ML {*
-fun all_inj_repabs_tac ctxt rel_refl trans2 =
- REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2)
+fun inj_repabs_tac ctxt =
+let
+ val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt)
+ val trans2 = map (OF1 @{thm equals_rsp}) (quotient_rules_get ctxt)
+in
+ inj_repabs_step_tac ctxt rel_refl trans2
+end
+
+fun all_inj_repabs_tac ctxt =
+ REPEAT_ALL_NEW (inj_repabs_tac ctxt)
*}
-section {* Cleaning of the theorem *}
+section {* Cleaning of the Theorem *}
ML {*
fun make_inst lhs t =
@@ -1017,7 +985,7 @@
val _ = tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te)));
val ti =
(let
- val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
+ val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm)
in
Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
@@ -1026,7 +994,7 @@
val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm)
val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te
in
- MetaSimplifier.rewrite_rule @{thms id_simps} td
+ MetaSimplifier.rewrite_rule (id_simps_get ctxt) td
end);
val _ = if not (Term.is_Const a2 andalso fst (dest_Const a2) = @{const_name "id"}) then
(tracing "lambda_prs";
@@ -1049,39 +1017,24 @@
fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
*}
-(*
- Cleaning the theorem consists of three rewriting steps.
- The first two need to be done before fun_map is unfolded
-
- 1) lambda_prs:
- (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) ----> f
-
- Implemented as conversion since it is not a pattern.
-
- 2) all_prs (the same for exists):
- Ball (Respects R) ((abs ---> id) f) ----> All f
-
- Rewriting with definitions from the argument defs
- (rep ---> abs) oldConst ----> newconst
-
- 3) Quotient_rel_rep:
- Rel (Rep x) (Rep y) ----> x = y
-
- Quotient_abs_rep:
- Abs (Rep x) ----> x
-
- id_simps; fun_map.simps
-*)
+(* 1. conversion (is not a pattern) *)
+thm lambda_prs
+(* 2. folding of definitions: (rep ---> abs) oldConst == newconst *)
+(* and simplification with *)
+thm all_prs ex_prs
+(* 3. simplification with *)
+thm fun_map.simps Quotient_abs_rep Quotient_rel_rep id_simps
+(* 4. Test for refl *)
ML {*
fun clean_tac lthy =
let
val thy = ProofContext.theory_of lthy;
val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
- (* FIXME: shouldn't the definitions already be varified? *)
+ (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *)
val thms1 = @{thms all_prs ex_prs} @ defs
- val thms2 = @{thms eq_reflection[OF fun_map.simps]}
- @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep}
+ val thms2 = @{thms eq_reflection[OF fun_map.simps]} @ (id_simps_get lthy)
+ @ @{thms Quotient_abs_rep Quotient_rel_rep}
fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
in
EVERY' [lambda_prs_tac lthy,
@@ -1091,7 +1044,7 @@
end
*}
-section {* Genralisation of free variables in a goal *}
+section {* Tactic for genralisation of free variables in a goal *}
ML {*
fun inst_spec ctrm =
@@ -1121,7 +1074,7 @@
end)
*}
-section {* General outline of the lifting procedure *}
+section {* General Shape of the Lifting Procedure *}
(* - A is the original raw theorem *)
(* - B is the regularized theorem *)
@@ -1138,8 +1091,8 @@
and c: "B = C"
and d: "C = D"
shows "D"
- using a b c d
- by simp
+using a b c d
+by simp
ML {*
fun lift_match_error ctxt fun_str rtrm qtrm =
@@ -1162,11 +1115,9 @@
val reg_goal =
Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm')
handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm
- val _ = warning "Regularization done."
val inj_goal =
Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm'))
handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm
- val _ = warning "RepAbs Injection done."
in
Drule.instantiate' []
[SOME (cterm_of thy rtrm'),
@@ -1175,42 +1126,40 @@
end
*}
-(* Left for debugging *)
ML {*
+(* the tactic leaves three subgoals to be proved *)
fun procedure_tac ctxt rthm =
ObjectLogic.full_atomize_tac
THEN' gen_frees_tac ctxt
- THEN' CSUBGOAL (fn (gl, i) =>
+ THEN' CSUBGOAL (fn (goal, i) =>
let
val rthm' = atomize_thm rthm
- val rule = procedure_inst ctxt (prop_of rthm') (term_of gl)
- val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i}
+ val rule = procedure_inst ctxt (prop_of rthm') (term_of goal)
+ val bare_goal = snd (Thm.dest_comb goal)
+ val quot_weak = Drule.instantiate' [] [SOME bare_goal] @{thm QUOT_TRUE_i}
in
- (rtac rule THEN' RANGE [rtac rthm', (fn _ => all_tac), rtac thm]) i
+ (rtac rule THEN' RANGE [rtac rthm', K all_tac, rtac quot_weak]) i
end)
*}
+(* automatic proofs *)
+ML {*
+fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac)
+
+fun WARN (tac, msg) i st =
+ case Seq.pull ((SOLVES' tac) i st) of
+ NONE => (warning msg; Seq.single st)
+ | seqcell => Seq.make (fn () => seqcell)
+
+fun RANGE_WARN xs = RANGE (map WARN xs)
+*}
+
ML {*
-(* FIXME/TODO should only get as arguments the rthm like procedure_tac *)
-
fun lift_tac ctxt rthm =
- ObjectLogic.full_atomize_tac
- THEN' gen_frees_tac ctxt
- THEN' CSUBGOAL (fn (gl, i) =>
- let
- val rthm' = atomize_thm rthm
- val rule = procedure_inst ctxt (prop_of rthm') (term_of gl)
- val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) (equiv_rules_get ctxt)
- val quotients = quotient_rules_get ctxt
- val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quotients
- val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i}
- in
- (rtac rule THEN'
- RANGE [rtac rthm',
- regularize_tac ctxt,
- rtac thm THEN' all_inj_repabs_tac ctxt rel_refl trans2,
- clean_tac ctxt]) i
- end)
+ procedure_tac ctxt rthm
+ THEN' RANGE_WARN [(regularize_tac ctxt, "Regularize proof failed."),
+ (all_inj_repabs_tac ctxt, "Injection proof failed."),
+ (clean_tac ctxt, "Cleaning proof failed.")]
*}
end
--- a/Quot/Quotients.thy Tue Dec 08 11:17:56 2009 +0100
+++ b/Quot/Quotients.thy Tue Dec 08 11:20:01 2009 +0100
@@ -42,10 +42,6 @@
"sum_map f1 f2 (Inl a) = Inl (f1 a)"
| "sum_map f1 f2 (Inr a) = Inr (f2 a)"
-
-
-
-
fun
noption_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)"
where
--- a/Quot/quotient_info.ML Tue Dec 08 11:17:56 2009 +0100
+++ b/Quot/quotient_info.ML Tue Dec 08 11:20:01 2009 +0100
@@ -26,6 +26,7 @@
val equiv_rules_get: Proof.context -> thm list
val equiv_rules_add: attribute
val rsp_rules_get: Proof.context -> thm list
+ val id_simps_get: Proof.context -> thm list
val quotient_rules_get: Proof.context -> thm list
val quotient_rules_add: attribute
end;
@@ -62,6 +63,10 @@
val tyname = Sign.intern_type thy tystr
val mapname = Sign.intern_const thy mapstr
val relname = Sign.intern_const thy relstr
+
+ fun check s = (Const (s, dummyT) |> Syntax.check_term ctxt)
+ handle _ => error ("Constant " ^ s ^ " not declared.")
+ val _ = map check [mapname, relname]
in
maps_attribute_aux tyname {mapfun = mapname, relfun = relname}
end
@@ -170,6 +175,9 @@
OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants"
OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of)))
+(* FIXME/TODO: check the various lemmas conform *)
+(* with the required shape *)
+
(* equivalence relation theorems *)
structure EquivRules = Named_Thms
(val name = "quotient_equiv"
@@ -185,6 +193,13 @@
val rsp_rules_get = RspRules.get
+(* respectfulness theorems *)
+structure IdSimps = Named_Thms
+ (val name = "id_simps"
+ val description = "Identity simp rules for maps.")
+
+val id_simps_get = IdSimps.get
+
(* quotient theorems *)
structure QuotientRules = Named_Thms
(val name = "quotient_thm"
@@ -197,6 +212,7 @@
val _ = Context.>> (Context.map_theory
(EquivRules.setup #>
RspRules.setup #>
+ IdSimps.setup #>
QuotientRules.setup))
end; (* structure *)