--- a/FSet.thy Mon Nov 30 12:26:08 2009 +0100
+++ b/FSet.thy Mon Nov 30 13:58:05 2009 +0100
@@ -295,8 +295,7 @@
ML {* val qty = @{typ "'a fset"} *}
ML {* val rsp_thms =
- @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp}
- @ @{thms ho_all_prs ho_ex_prs} *}
+ @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_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} "fset"; *}
@@ -506,20 +505,20 @@
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
-apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
+apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
apply assumption
apply (rule refl)
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
-apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
+apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
apply (tactic {* REPEAT_ALL_NEW (inj_repabs_tac_fset @{context}) 1 *})
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
-apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
+apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
--- a/IntEx.thy Mon Nov 30 12:26:08 2009 +0100
+++ b/IntEx.thy Mon Nov 30 13:58:05 2009 +0100
@@ -134,7 +134,7 @@
ML {* val qty = @{typ "my_int"} *}
ML {* val ty_name = "my_int" *}
-ML {* val rsp_thms = @{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs} *}
+ML {* val rsp_thms = @{thms ho_plus_rsp} *}
ML {* val defs = @{thms PLUS_def} *}
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"; *}
--- a/LFex.thy Mon Nov 30 12:26:08 2009 +0100
+++ b/LFex.thy Mon Nov 30 13:58:05 2009 +0100
@@ -214,13 +214,23 @@
thm akind_aty_atrm.induct
-
+thm kind_ty_trm.induct
ML {* val defs =
@{thms TYP_def KPI_def TCONST_def TAPP_def TPI_def VAR_def CONS_def APP_def LAM_def
FV_kind_def FV_ty_def FV_trm_def perm_kind_def perm_ty_def perm_trm_def}
*}
+ML {*
+ val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM}
+ val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs}
+ val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) @{thms alpha_EQUIVs}
+ val lower = flat (map (add_lower_defs @{context}) defs)
+ val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower
+ val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot
+ val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same
+*}
+
lemma
assumes a0:
"P1 TYP TYP"
@@ -260,12 +270,6 @@
ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm akind_aty_atrm.induct})) (term_of qtm) *}
apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
-(* injecting *)
-ML_prf {* val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} *}
-ML_prf {*
- val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs}
- val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) @{thms alpha_EQUIVs}
-*}
apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
@@ -457,14 +461,8 @@
apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*})
-(* cleaning *)
-ML_prf {* val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} *}
(*apply(tactic {* clean_tac @{context} quot defs aps 1 *}) *)
apply (tactic {* lambda_prs_tac @{context} quot 1 *})
-ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *}
-ML_prf {* val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower *}
-ML_prf {* val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot *}
-ML_prf {* val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same *}
apply (tactic {* simp_tac ((Simplifier.context @{context} empty_ss) addsimps (meta_reps_same @ meta_lower)) 1 *})
apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *})
ML_prf {* val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot *}
@@ -494,6 +492,131 @@
apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
done
+(* Does not work:
+lemma
+ assumes a0: "P1 TYP"
+ and a1: "\<And>ty name kind. \<lbrakk>P2 ty; P1 kind\<rbrakk> \<Longrightarrow> P1 (KPI ty name kind)"
+ and a2: "\<And>id. P2 (TCONST id)"
+ and a3: "\<And>ty trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P2 (TAPP ty trm)"
+ and a4: "\<And>ty1 name ty2. \<lbrakk>P2 ty1; P2 ty2\<rbrakk> \<Longrightarrow> P2 (TPI ty1 name ty2)"
+ and a5: "\<And>id. P3 (CONS id)"
+ and a6: "\<And>name. P3 (VAR name)"
+ and a7: "\<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2)"
+ and a8: "\<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)"
+ shows "P1 mkind \<and> P2 mty \<and> P3 mtrm"
+using a0 a1 a2 a3 a4 a5 a6 a7 a8
+*)
+
+lemma "\<lbrakk>P1 TYP;
+ \<And>ty name kind. \<lbrakk>P2 ty; P1 kind\<rbrakk> \<Longrightarrow> P1 (KPI ty name kind);
+ \<And>id. P2 (TCONST id);
+ \<And>ty trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P2 (TAPP ty trm);
+ \<And>ty1 name ty2. \<lbrakk>P2 ty1; P2 ty2\<rbrakk> \<Longrightarrow> P2 (TPI ty1 name ty2);
+ \<And>id. P3 (CONS id); \<And>name. P3 (VAR name);
+ \<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 {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
+ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
+ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm kind_ty_trm.induct})) (term_of qtm) *}
+apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *})
+apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
+prefer 2
+apply(tactic {* clean_tac @{context} quot defs aps 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+(* LOOP! *)
+(* apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) *)
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *})
+done
+
print_quotients
end
--- a/LamEx.thy Mon Nov 30 12:26:08 2009 +0100
+++ b/LamEx.thy Mon Nov 30 13:58:05 2009 +0100
@@ -171,8 +171,7 @@
ML {* val qty = @{typ "lam"} *}
ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def fv_def} *}
-ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} @
- @{thms ho_all_prs ho_ex_prs} *}
+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 consts = lookup_quot_consts defs *}
--- a/QuotMain.thy Mon Nov 30 12:26:08 2009 +0100
+++ b/QuotMain.thy Mon Nov 30 13:58:05 2009 +0100
@@ -136,6 +136,7 @@
end
+(* EQUALS_RSP is stronger *)
lemma equiv_trans2:
assumes e: "EQUIV R"
and ac: "R a c"
@@ -927,13 +928,13 @@
NDT ctxt "2" (lambda_res_tac ctxt),
(* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
- NDT ctxt "3" (rtac @{thm RES_FORALL_RSP}),
+ NDT ctxt "3" (rtac @{thm ball_rsp}),
(* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *)
NDT ctxt "4" (ball_rsp_tac ctxt),
(* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
- NDT ctxt "5" (rtac @{thm RES_EXISTS_RSP}),
+ NDT ctxt "5" (rtac @{thm bex_rsp}),
(* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *)
NDT ctxt "6" (bex_rsp_tac ctxt),
@@ -946,7 +947,7 @@
(* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
(* observe ---> *)
- NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt
+ NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt
THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))),
(* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP provided type of t needs lifting *)
@@ -1030,8 +1031,7 @@
ML {*
fun allex_prs_tac lthy quot =
- (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})
- THEN' (quotient_tac quot)
+ (EqSubst.eqsubst_tac lthy [0] @{thms all_prs ex_prs}) THEN' (quotient_tac quot)
*}
(* Rewrites the term with LAMBDA_PRS thm.
@@ -1102,6 +1102,25 @@
Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i)
*}
+(*
+ Cleaning the theorem consists of 5 kinds of rewrites.
+ These rewrites can be done independently and in any order.
+
+ - LAMBDA_PRS:
+ (Rep1 ---> Abs2) (\<lambda>x. Rep2 (?f (Abs1 x))) \<equiv> ?f
+ - Rewriting with definitions from the argument defs
+ (Abs) OldConst (Rep Args) \<equiv> NewConst Args
+ - QUOTIENT_REL_REP:
+ Rel (Rep x) (Rep y) \<equiv> x = y
+ - FORALL_PRS (and the same for exists: EXISTS_PRS)
+ \<forall>x\<in>Respects R. (abs ---> id) ?f \<equiv> \<forall>x. ?f
+ - applic_prs
+ Abs1 ((Abs2 --> Rep1) f (Rep2 args)) \<equiv> f args
+
+ The first one is implemented as a conversion (fast).
+ The second and third one are a simp_tac (fast).
+ The last two are EqSubst (slow).
+*)
ML {*
fun clean_tac lthy quot defs aps =
let
--- a/QuotScript.thy Mon Nov 30 12:26:08 2009 +0100
+++ b/QuotScript.thy Mon Nov 30 13:58:05 2009 +0100
@@ -68,14 +68,14 @@
by blast
lemma QUOTIENT_REL_REP:
- assumes a: "QUOTIENT E Abs Rep"
- shows "E (Rep a) (Rep b) = (a = b)"
+ assumes a: "QUOTIENT R Abs Rep"
+ shows "R (Rep a) (Rep b) = (a = b)"
using a unfolding QUOTIENT_def
by metis
lemma QUOTIENT_REP_ABS:
- assumes a: "QUOTIENT E Abs Rep"
- shows "E r r \<Longrightarrow> E (Rep (Abs r)) r"
+ assumes a: "QUOTIENT R Abs Rep"
+ shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
using a unfolding QUOTIENT_def
by blast
@@ -223,6 +223,7 @@
using FUN_QUOTIENT[OF q1 q2] unfolding Respects_def QUOTIENT_def expand_fun_eq
by blast
+(* TODO: it is the same as APPLY_RSP *)
(* q1 and q2 not used; see next lemma *)
lemma FUN_REL_MP:
assumes q1: "QUOTIENT R1 Abs1 Rep1"
@@ -259,10 +260,11 @@
using q1 q2 r1 r2 a
by (simp add: FUN_REL_EQUALS)
+(* We don't use it, it is exactly the same as QUOTIENT_REL_REP but wrong way *)
lemma EQUALS_PRS:
assumes q: "QUOTIENT R Abs Rep"
shows "(x = y) = R (Rep x) (Rep y)"
-by (simp add: QUOTIENT_REL_REP[OF q])
+by (rule QUOTIENT_REL_REP[OF q, symmetric])
lemma EQUALS_RSP:
assumes q: "QUOTIENT R Abs Rep"
@@ -285,8 +287,9 @@
shows "(\<lambda>x. f x) = (Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x)"
unfolding expand_fun_eq
using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2]
-by (simp)
+by simp
+(* Not used since applic_prs proves a version for an arbitrary number of arguments *)
lemma APP_PRS:
assumes q1: "QUOTIENT R1 abs1 rep1"
and q2: "QUOTIENT R2 abs2 rep2"
@@ -320,25 +323,21 @@
assumes q: "QUOTIENT R Abs Rep"
and a: "R x1 x2"
shows "R x1 (Rep (Abs x2))"
+using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q])
+
+(* Not used *)
+lemma REP_ABS_RSP_LEFT:
+ assumes q: "QUOTIENT R Abs Rep"
+ and a: "R x1 x2"
and "R (Rep (Abs x1)) x2"
-proof -
- show "R x1 (Rep (Abs x2))"
- using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q])
-next
- show "R (Rep (Abs x1)) x2"
- using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q] QUOTIENT_SYM[of q])
-qed
+ shows "R x1 (Rep (Abs x2))"
+using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q] QUOTIENT_SYM[of q])
(* ----------------------------------------------------- *)
(* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE, *)
(* RES_FORALL, RES_EXISTS, RES_EXISTS_EQUIV *)
(* ----------------------------------------------------- *)
-(* what is RES_FORALL *)
-(*--`!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
- !f. $! f = RES_FORALL (respects R) ((abs --> I) f)`--*)
-(*as peter here *)
-
(* bool theory: COND, LET *)
lemma IF_PRS:
@@ -398,6 +397,7 @@
(* combinators: I, K, o, C, W *)
+(* We use id_simps which includes id_apply; so these 2 theorems can be removed *)
lemma I_PRS:
assumes q: "QUOTIENT R Abs Rep"
shows "id e = Abs (id (Rep e))"
@@ -430,6 +430,17 @@
+
+
+lemma COND_PRS:
+ assumes a: "QUOTIENT R absf repf"
+ shows "(if a then b else c) = absf (if a then repf b else repf c)"
+ using a unfolding QUOTIENT_def by auto
+
+
+
+
+
(* Set of lemmas for regularisation of ball and bex *)
lemma ball_reg_eqv:
fixes P :: "'a \<Rightarrow> bool"
@@ -525,49 +536,29 @@
"((\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)) \<Longrightarrow> ((\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y))"
by auto
-
-
-(* TODO: Add similar *)
-lemma RES_FORALL_RSP:
- shows "\<And>f g. (R ===> (op =)) f g ==>
- (Ball (Respects R) f = Ball (Respects R) g)"
- apply (simp add: FUN_REL.simps Ball_def IN_RESPECTS)
- done
+(* 2 lemmas needed for proving repabs_inj *)
+lemma ball_rsp:
+ assumes a: "(R ===> (op =)) f g"
+ shows "Ball (Respects R) f = Ball (Respects R) g"
+ using a by (simp add: Ball_def IN_RESPECTS)
-lemma RES_EXISTS_RSP:
- shows "\<And>f g. (R ===> (op =)) f g ==>
- (Bex (Respects R) f = Bex (Respects R) g)"
- apply (simp add: FUN_REL.simps Bex_def IN_RESPECTS)
- done
+lemma bex_rsp:
+ assumes a: "(R ===> (op =)) f g"
+ shows "(Bex (Respects R) f = Bex (Respects R) g)"
+ using a by (simp add: Bex_def IN_RESPECTS)
-
-lemma FORALL_PRS:
+(* 2 lemmas needed for cleaning of quantifiers *)
+lemma all_prs:
assumes a: "QUOTIENT R absf repf"
- shows "All f = Ball (Respects R) ((absf ---> id) f)"
- using a
- unfolding QUOTIENT_def
+ shows "Ball (Respects R) ((absf ---> id) f) = All f"
+ using a unfolding QUOTIENT_def
by (metis IN_RESPECTS fun_map.simps id_apply)
-lemma EXISTS_PRS:
- assumes a: "QUOTIENT R absf repf"
- shows "Ex f = Bex (Respects R) ((absf ---> id) f)"
- using a
- unfolding QUOTIENT_def
- by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply mem_def)
-
-lemma COND_PRS:
+lemma ex_prs:
assumes a: "QUOTIENT R absf repf"
- shows "(if a then b else c) = absf (if a then repf b else repf c)"
- using a unfolding QUOTIENT_def by auto
-
-(* These are the fixed versions, general ones need to be proved. *)
-lemma ho_all_prs:
- shows "((op = ===> op =) ===> op =) All All"
- by auto
-
-lemma ho_ex_prs:
- shows "((op = ===> op =) ===> op =) Ex Ex"
- by auto
+ shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
+ using a unfolding QUOTIENT_def
+ by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply)
end