The big merge; probably non-functional.
--- a/FIXME-TODO Fri Dec 04 09:08:51 2009 +0100
+++ b/FIXME-TODO Fri Dec 04 09:25:27 2009 +0100
@@ -27,7 +27,15 @@
Lower Priority
==============
+- allow the user to provide the rsp lemmas in a more
+ natural form
+
- find clean ways how to write down the "mathematical"
procedure for a possible submission (Peter submitted
his work only to TPHOLs 2005...we would have to go
maybe for the Journal of Formalised Mathematics)
+
+- use lower-case letters where appropriate in order
+ to make Markus happy
+
+- add tests for adding theorems to the various thm lists
\ No newline at end of file
--- a/FSet.thy Fri Dec 04 09:08:51 2009 +0100
+++ b/FSet.thy Fri Dec 04 09:25:27 2009 +0100
@@ -135,9 +135,6 @@
if (a memb A) then (fold1 f g z A) else (f (g a) (fold1 f g z A))
) else z)"
-(* fold1_def is not usable, but: *)
-thm fold1.simps
-
lemma fs1_strong_cases:
fixes X :: "'a list"
shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a memb Y) \<and> (X \<approx> a # Y)))"
@@ -180,7 +177,7 @@
shows "(z memb x) = (z memb y)"
using a by induct auto
-lemma ho_memb_rsp[quot_rsp]:
+lemma ho_memb_rsp[quotient_rsp]:
"(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)"
by (simp add: memb_rsp)
@@ -190,17 +187,17 @@
shows "card1 a = card1 b"
using e by induct (simp_all add:memb_rsp)
-lemma ho_card1_rsp[quot_rsp]:
+lemma ho_card1_rsp[quotient_rsp]:
"(op \<approx> ===> op =) card1 card1"
by (simp add: card1_rsp)
-lemma cons_rsp[quot_rsp]:
+lemma cons_rsp[quotient_rsp]:
fixes z
assumes a: "xs \<approx> ys"
shows "(z # xs) \<approx> (z # ys)"
using a by (rule list_eq.intros(5))
-lemma ho_cons_rsp[quot_rsp]:
+lemma ho_cons_rsp[quotient_rsp]:
"(op = ===> op \<approx> ===> op \<approx>) op # op #"
by (simp add: cons_rsp)
@@ -257,7 +254,7 @@
apply (rule append_sym_rsp)
done
-lemma ho_append_rsp[quot_rsp]:
+lemma ho_append_rsp[quotient_rsp]:
"(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
by (simp add: append_rsp)
@@ -269,7 +266,7 @@
apply(auto intro: list_eq.intros)
done
-lemma ho_map_rsp[quot_rsp]:
+lemma ho_map_rsp[quotient_rsp]:
"(op = ===> op \<approx> ===> op \<approx>) map map"
by (simp add: map_rsp)
@@ -277,7 +274,7 @@
"(map f (a @ b)) \<approx> (map f a) @ (map f b)"
by simp (rule list_eq_refl)
-lemma ho_fold_rsp[quot_rsp]:
+lemma ho_fold_rsp[quotient_rsp]:
"(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1"
apply (auto simp add: FUN_REL_EQ)
apply (case_tac "rsp_fold x")
@@ -297,13 +294,13 @@
ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *}
-ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] [quot] *}
+ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *}
lemma "IN x EMPTY = False"
apply(tactic {* procedure_tac @{context} @{thm m1} 1 *})
apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply(tactic {* clean_tac @{context} [quot] 1*})
+apply(tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply(tactic {* clean_tac @{context} 1*})
done
lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"
@@ -330,7 +327,7 @@
apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
done
-ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [quot] [rel_refl] [trans2] *}
+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 *})
@@ -348,7 +345,7 @@
apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
prefer 2
-apply(tactic {* clean_tac @{context} [quot] 1 *})
+apply(tactic {* clean_tac @{context} 1 *})
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
@@ -404,6 +401,9 @@
apply (assumption)
done
+ML {* quot *}
+thm quotient_thm
+
lemma "P (x :: 'a list) (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
@@ -431,8 +431,8 @@
"INSERT2 \<equiv> op #"
ML {* val quot = @{thms QUOTIENT_fset QUOTIENT_fset2} *}
-ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy quot [rel_refl] [trans2] *}
-ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] quot *}
+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 [rel_eqv] *}
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 *})
@@ -453,20 +453,20 @@
"fset_case \<equiv> list_case"
(* Probably not true without additional assumptions about the function *)
-lemma list_rec_rsp[quot_rsp]:
+lemma list_rec_rsp[quotient_rsp]:
"(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec"
apply (auto simp add: FUN_REL_EQ)
apply (erule_tac list_eq.induct)
apply (simp_all)
sorry
-lemma list_case_rsp[quot_rsp]:
+lemma list_case_rsp[quotient_rsp]:
"(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
apply (auto simp add: FUN_REL_EQ)
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 [rel_eqv] quot *}
+ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *}
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 *})
--- a/IntEx.thy Fri Dec 04 09:08:51 2009 +0100
+++ b/IntEx.thy Fri Dec 04 09:25:27 2009 +0100
@@ -13,6 +13,8 @@
apply(auto simp add: mem_def expand_fun_eq)
done
+thm quotient_thm
+
thm my_int_equiv
print_theorems
@@ -129,7 +131,7 @@
apply(auto)
done
-lemma ho_plus_rsp[quot_rsp]:
+lemma ho_plus_rsp[quotient_rsp]:
shows "(intrel ===> intrel ===> intrel) my_plus my_plus"
by (simp)
@@ -139,17 +141,17 @@
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 [rel_eqv] [quot] *}
+ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] *}
-ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [quot] [rel_refl] [trans2] *}
-ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [quot] [rel_refl] [trans2] *}
+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 "PLUS a b = PLUS b a"
apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
prefer 2
-apply(tactic {* clean_tac @{context} [quot] 1 *})
+apply(tactic {* clean_tac @{context} 1 *})
apply(tactic {* inj_repabs_tac_intex @{context} 1*})
apply(tactic {* inj_repabs_tac_intex @{context} 1*})
apply(tactic {* inj_repabs_tac_intex @{context} 1*})
@@ -187,7 +189,7 @@
apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* clean_tac @{context} [quot] 1 *})
+apply(tactic {* clean_tac @{context} 1 *})
done
lemma ho_tst: "foldl my_plus x [] = x"
@@ -234,12 +236,12 @@
apply (induct t)
by (simp_all add: QUOTIENT_ABS_REP[OF a])
-lemma cons_rsp[quot_rsp]:
+lemma cons_rsp[quotient_rsp]:
"(op \<approx> ===> LIST_REL op \<approx> ===> LIST_REL op \<approx>) op # op #"
by simp
(* I believe it's true. *)
-lemma foldl_rsp[quot_rsp]:
+lemma foldl_rsp[quotient_rsp]:
"((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> LIST_REL op \<approx> ===> op \<approx>) foldl foldl"
apply (simp only: FUN_REL.simps)
apply (rule allI)
@@ -254,37 +256,17 @@
apply (induct_tac xb yb rule: list_induct2) (* To finish I need to give it: arbitrary:xa ya *)
sorry
-lemma nil_listrel_rsp[quot_rsp]:
+lemma nil_listrel_rsp[quotient_rsp]:
"(LIST_REL R) [] []"
by simp
-thm LAMBDA_PRS[no_vars]
-thm all_prs[no_vars]
-
-lemma test_all_prs:
- "\<lbrakk>QUOTIENT R absf repf; f = g\<rbrakk> \<Longrightarrow> Ball (Respects R) ((absf ---> id) f) = All g"
-apply(drule all_prs)
-apply(simp)
-done
-
-lemma test:
- "\<lbrakk>QUOTIENT R1 Abs1 Rep1; QUOTIENT R2 Abs2 Rep2;
- (\<lambda>x. Rep2 (f (Abs1 x))) = lhs \<rbrakk> \<Longrightarrow> (Rep1 ---> Abs2) lhs = f"
-apply -
-thm LAMBDA_PRS
-apply(drule LAMBDA_PRS)
-apply(assumption)
-apply(auto)
-done
-
-
lemma "foldl PLUS x [] = x"
apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})
apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int])
apply(simp only: nil_prs)
-apply(tactic {* clean_tac @{context} [quot] 1 *})
+apply(tactic {* clean_tac @{context} 1 *})
done
lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)"
@@ -296,6 +278,6 @@
apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int])
apply(simp only: cons_prs[OF QUOTIENT_my_int])
-apply(tactic {* clean_tac @{context} [quot] 1 *})
+apply(tactic {* clean_tac @{context} 1 *})
done
--- a/LFex.thy Fri Dec 04 09:08:51 2009 +0100
+++ b/LFex.thy Fri Dec 04 09:25:27 2009 +0100
@@ -181,35 +181,35 @@
"perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"
(* TODO/FIXME: Think whether these RSP theorems are true. *)
-lemma kpi_rsp[quot_rsp]:
+lemma kpi_rsp[quotient_rsp]:
"(aty ===> op = ===> akind ===> akind) KPi KPi" sorry
-lemma tconst_rsp[quot_rsp]:
+lemma tconst_rsp[quotient_rsp]:
"(op = ===> aty) TConst TConst" sorry
-lemma tapp_rsp[quot_rsp]:
+lemma tapp_rsp[quotient_rsp]:
"(aty ===> atrm ===> aty) TApp TApp" sorry
-lemma tpi_rsp[quot_rsp]:
+lemma tpi_rsp[quotient_rsp]:
"(aty ===> op = ===> aty ===> aty) TPi TPi" sorry
-lemma var_rsp[quot_rsp]:
+lemma var_rsp[quotient_rsp]:
"(op = ===> atrm) Var Var" sorry
-lemma app_rsp[quot_rsp]:
+lemma app_rsp[quotient_rsp]:
"(atrm ===> atrm ===> atrm) App App" sorry
-lemma const_rsp[quot_rsp]:
+lemma const_rsp[quotient_rsp]:
"(op = ===> atrm) Const Const" sorry
-lemma lam_rsp[quot_rsp]:
+lemma lam_rsp[quotient_rsp]:
"(aty ===> op = ===> atrm ===> atrm) Lam Lam" sorry
-lemma perm_kind_rsp[quot_rsp]:
+lemma perm_kind_rsp[quotient_rsp]:
"(op = ===> akind ===> akind) op \<bullet> op \<bullet>" sorry
-lemma perm_ty_rsp[quot_rsp]:
+lemma perm_ty_rsp[quotient_rsp]:
"(op = ===> aty ===> aty) op \<bullet> op \<bullet>" sorry
-lemma perm_trm_rsp[quot_rsp]:
+lemma perm_trm_rsp[quotient_rsp]:
"(op = ===> atrm ===> atrm) op \<bullet> op \<bullet>" sorry
-lemma fv_ty_rsp[quot_rsp]:
+lemma fv_ty_rsp[quotient_rsp]:
"(aty ===> op =) fv_ty fv_ty" sorry
-lemma fv_kind_rsp[quot_rsp]:
+lemma fv_kind_rsp[quotient_rsp]:
"(akind ===> op =) fv_kind fv_kind" sorry
-lemma fv_trm_rsp[quot_rsp]:
+lemma fv_trm_rsp[quotient_rsp]:
"(atrm ===> op =) fv_trm fv_trm" sorry
@@ -261,7 +261,7 @@
apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
prefer 2
-apply(tactic {* clean_tac @{context} quot 1 *})
+apply(tactic {* clean_tac @{context} 1 *})
(*
Profiling:
ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *}
@@ -270,8 +270,8 @@
ML_prf {* PolyML.profiling 1 *}
ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *}
*)
-apply(tactic {* all_inj_repabs_tac' @{context} quot rel_refl trans2 1 *})
-(*apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *})*)
+apply(tactic {* all_inj_repabs_tac' @{context} rel_refl trans2 1 *})
+(*apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})*)
done
(* Does not work:
@@ -298,7 +298,7 @@
\<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2);
\<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk>
\<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm"
-apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} @{thms alpha_EQUIVs} quot 1 *})
+apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} @{thms alpha_EQUIVs} 1 *})
done
print_quotients
--- a/LamEx.thy Fri Dec 04 09:08:51 2009 +0100
+++ b/LamEx.thy Fri Dec 04 09:25:27 2009 +0100
@@ -128,7 +128,7 @@
unfolding fresh_def supp_def
sorry
-lemma perm_rsp[quot_rsp]:
+lemma perm_rsp[quotient_rsp]:
"(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>"
apply(auto)
(* this is propably true if some type conditions are imposed ;o) *)
@@ -140,14 +140,14 @@
(* this is probably only true if some type conditions are imposed *)
sorry
-lemma rVar_rsp[quot_rsp]:
+lemma rVar_rsp[quotient_rsp]:
"(op = ===> alpha) rVar rVar"
by (auto intro:a1)
-lemma rApp_rsp[quot_rsp]: "(alpha ===> alpha ===> alpha) rApp rApp"
+lemma rApp_rsp[quotient_rsp]: "(alpha ===> alpha ===> alpha) rApp rApp"
by (auto intro:a2)
-lemma rLam_rsp[quot_rsp]: "(op = ===> alpha ===> alpha) rLam rLam"
+lemma rLam_rsp[quotient_rsp]: "(op = ===> alpha ===> alpha) rLam rLam"
apply(auto)
apply(rule a3)
apply(rule_tac t="[(x,x)]\<bullet>y" and s="y" in subst)
@@ -160,7 +160,7 @@
apply(simp add: abs_fresh)
done
-lemma rfv_rsp[quot_rsp]: "(alpha ===> op =) rfv rfv"
+lemma rfv_rsp[quotient_rsp]: "(alpha ===> op =) rfv rfv"
sorry
lemma rvar_inject: "rVar a \<approx> rVar b = (a = b)"
@@ -174,7 +174,7 @@
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 [rel_eqv] [quot] *}
+ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] *}
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 *})
@@ -312,39 +312,32 @@
"\<lbrakk>t = [(a, b)] \<bullet> s; a \<sharp> [b].s\<rbrakk> \<Longrightarrow> Lam a t = Lam b s"
apply (tactic {* procedure_tac @{context} @{thm real_alpha_pre} 1 *})
prefer 2
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* all_inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
apply (simp only: perm_prs)
prefer 2
-apply (tactic {* all_inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
+apply (tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
prefer 3
-apply (tactic {* clean_tac @{context} [quot] 1 *})
-
-thm all_prs
-thm REP_ABS_RSP
-thm ball_reg_eqv_range
-
-
-thm perm_lam_def
+apply (tactic {* clean_tac @{context} 1 *})
apply (simp only: perm_prs)
-(*apply (tactic {* regularize_tac @{context} [quot] 1 *})*)
+(*apply (tactic {* regularize_tac @{context} 1 *})*)
sorry
done
--- a/QuotList.thy Fri Dec 04 09:08:51 2009 +0100
+++ b/QuotList.thy Fri Dec 04 09:25:27 2009 +0100
@@ -15,7 +15,7 @@
| "LIST_REL R (x#xs) (y#ys) = (R x y \<and> LIST_REL R xs ys)"
lemma LIST_REL_EQ:
- shows "LIST_REL (op =) = (op =)"
+ shows "LIST_REL (op =) \<equiv> (op =)"
unfolding expand_fun_eq
apply(rule allI)+
apply(induct_tac x xa rule: list_induct2')
--- a/QuotMain.thy Fri Dec 04 09:08:51 2009 +0100
+++ b/QuotMain.thy Fri Dec 04 09:25:27 2009 +0100
@@ -155,6 +155,9 @@
declare [[map * = (prod_fun, prod_rel)]]
declare [[map "fun" = (fun_map, FUN_REL)]]
+lemmas [quotient_thm] =
+ FUN_QUOTIENT IDENTITY_QUOTIENT LIST_QUOTIENT
+
ML {* maps_lookup @{theory} "List.list" *}
ML {* maps_lookup @{theory} "*" *}
ML {* maps_lookup @{theory} "fun" *}
@@ -730,15 +733,10 @@
*}
ML {*
-fun quotient_tac ctxt quot_thms =
+fun quotient_tac ctxt =
REPEAT_ALL_NEW (FIRST'
- [rtac @{thm FUN_QUOTIENT},
- resolve_tac quot_thms,
- rtac @{thm IDENTITY_QUOTIENT},
- rtac @{thm LIST_QUOTIENT},
- (* For functional identity quotients, (op = ---> op =) *)
- (* TODO: think about the other way around, if we need to shorten the relation *)
- CHANGED o (simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms id_simps}))])
+ [rtac @{thm IDENTITY_QUOTIENT},
+ resolve_tac (quotient_rules_get ctxt)])
*}
lemma FUN_REL_I:
@@ -901,7 +899,7 @@
ML {*
-fun inj_repabs_tac ctxt quot_thms rel_refl trans2 =
+fun inj_repabs_tac ctxt rel_refl trans2 =
(FIRST' [
(* "cong" rule of the of the relation / transitivity*)
(* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *)
@@ -933,11 +931,11 @@
(* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
(* observe ---> *)
NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt
- THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms)]))),
+ THEN' (RANGE [SOLVES' (quotient_tac ctxt)]))),
(* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP provided type of t needs lifting *)
NDT ctxt "A" (APPLY_RSP_TAC ctxt THEN'
- (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms),
+ (RANGE [SOLVES' (quotient_tac ctxt), SOLVES' (quotient_tac ctxt),
quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
(* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *)
@@ -953,16 +951,17 @@
NDT ctxt "D" (resolve_tac rel_refl),
(* resolving with R x y assumptions *)
- NDT ctxt "E" (atac),
+ NDT ctxt "E" (atac)
(* (op =) ===> (op =) \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *)
(* global simplification *)
- NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))])
+ (*NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms FUN_REL_EQ LIST_REL_EQ})))*)
+ ])
*}
ML {*
-fun all_inj_repabs_tac ctxt quot_thms rel_refl trans2 =
- REPEAT_ALL_NEW (inj_repabs_tac ctxt quot_thms rel_refl trans2)
+fun all_inj_repabs_tac ctxt rel_refl trans2 =
+ REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2)
*}
(* A faster version *)
@@ -1024,10 +1023,12 @@
(* TODO: This is slow *)
+(*
ML {*
-fun allex_prs_tac ctxt quot =
- (EqSubst.eqsubst_tac ctxt [0] @{thms all_prs ex_prs}) THEN' (quotient_tac ctxt quot)
+fun allex_prs_tac ctxt =
+ (EqSubst.eqsubst_tac ctxt [0] @{thms all_prs ex_prs}) THEN' (quotient_tac ctxt)
*}
+*)
ML {*
fun make_inst lhs t =
@@ -1046,11 +1047,11 @@
(* It proves the QUOTIENT assumptions by calling quotient_tac *)
ML {*
-fun solve_quotient_assum i quot_thms ctxt thm =
+fun solve_quotient_assum i ctxt thm =
let
val tac =
(compose_tac (false, thm, i)) THEN_ALL_NEW
- (quotient_tac ctxt quot_thms);
+ (quotient_tac ctxt);
val gc = Drule.strip_imp_concl (cprop_of thm);
in
Goal.prove_internal [] gc (fn _ => tac 1)
@@ -1059,7 +1060,7 @@
*}
ML {*
-fun lambda_allex_prs_simple_conv quot_thms ctxt ctrm =
+fun lambda_allex_prs_simple_conv ctxt ctrm =
case (term_of ctrm) of
((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
let
@@ -1070,7 +1071,7 @@
val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_d];
val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS};
- val te = @{thm eq_reflection} OF [solve_quotient_assum 2 quot_thms ctxt lpi]
+ val te = @{thm eq_reflection} OF [solve_quotient_assum 2 ctxt lpi]
val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
val tl = Thm.lhs_of ts;
val (insp, inst) = make_inst (term_of tl) (term_of ctrm);
@@ -1087,7 +1088,7 @@
val tyinst = [SOME cty_a, SOME cty_b];
val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)];
val thm = Drule.instantiate' tyinst tinst @{thm all_prs};
- val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 quot_thms ctxt thm];
+ val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 ctxt thm];
in
Conv.rewr_conv ti ctrm
end
@@ -1100,7 +1101,7 @@
val tyinst = [SOME cty_a, SOME cty_b];
val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)];
val thm = Drule.instantiate' tyinst tinst @{thm ex_prs};
- val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 quot_thms ctxt thm];
+ val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 ctxt thm];
in
Conv.rewr_conv ti ctrm
end
@@ -1110,12 +1111,12 @@
(* quot stands for the QUOTIENT theorems: *)
(* could be potentially all of them *)
ML {*
-fun lambda_allex_prs_conv quot =
- More_Conv.top_conv (lambda_allex_prs_simple_conv quot)
+val lambda_allex_prs_conv =
+ More_Conv.top_conv lambda_allex_prs_simple_conv
*}
ML {*
-fun lambda_allex_prs_tac quot ctxt = CONVERSION (lambda_allex_prs_conv quot ctxt)
+fun lambda_allex_prs_tac ctxt = CONVERSION (lambda_allex_prs_conv ctxt)
*}
(*
@@ -1145,13 +1146,14 @@
*)
ML {*
-fun clean_tac lthy quot =
+fun clean_tac lthy =
let
val thy = ProofContext.theory_of lthy;
+ val quotients = quotient_rules_get lthy
val defs = map (Thm.varifyT o #def) (qconsts_dest thy);
- val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot
+ val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quotients
val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep;
- val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot
+ val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quotients
val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same
val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps
(@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs)
@@ -1159,7 +1161,7 @@
EVERY' [
(* (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) ----> f *)
(* \<forall>x\<in>Respects R. (abs ---> id) f ----> \<forall>x. f *)
- NDT lthy "a" (TRY o lambda_allex_prs_tac quot lthy),
+ NDT lthy "a" (TRY o lambda_allex_prs_tac lthy),
(* NewConst ----> (rep ---> abs) oldConst *)
(* Abs (Rep x) ----> x *)
@@ -1272,7 +1274,7 @@
ML {*
(* FIXME/TODO should only get as arguments the rthm like procedure_tac *)
-fun lift_tac lthy rthm rel_eqv quot =
+fun lift_tac lthy rthm rel_eqv =
ObjectLogic.full_atomize_tac
THEN' gen_frees_tac lthy
THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
@@ -1287,8 +1289,8 @@
[rtac rule,
RANGE [rtac rthm',
regularize_tac lthy rel_eqv,
- rtac thm THEN' all_inj_repabs_tac' lthy quot rel_refl trans2,
- clean_tac lthy quot]]
+ rtac thm THEN' all_inj_repabs_tac' lthy rel_refl trans2,
+ clean_tac lthy]]
end) lthy
*}
--- a/QuotScript.thy Fri Dec 04 09:08:51 2009 +0100
+++ b/QuotScript.thy Fri Dec 04 09:25:27 2009 +0100
@@ -136,7 +136,7 @@
"E1 ===> E2 \<equiv> FUN_REL E1 E2"
lemma FUN_REL_EQ:
- "(op =) ===> (op =) = (op =)"
+ "(op =) ===> (op =) \<equiv> (op =)"
by (simp add: expand_fun_eq)
lemma FUN_QUOTIENT:
--- a/quotient_info.ML Fri Dec 04 09:08:51 2009 +0100
+++ b/quotient_info.ML Fri Dec 04 09:25:27 2009 +0100
@@ -164,14 +164,14 @@
(* respectfulness lemmas *)
structure RspRules = Named_Thms
- (val name = "quot_rsp"
+ (val name = "quotient_rsp"
val description = "Respectfulness theorems.")
val rsp_rules_get = RspRules.get
(* quotient lemmas *)
structure QuotientRules = Named_Thms
- (val name = "quotient"
+ (val name = "quotient_thm"
val description = "Quotient theorems.")
val quotient_rules_get = QuotientRules.get