# HG changeset patch # User Christian Urban # Date 1259585885 -3600 # Node ID 40c9fb60de3cfed4fd4d0f4bf879115bf038b542 # Parent 3f8c7183ddacdf8d3435e2da8e0a1a6c78d95ddc# Parent 020e27417b59882e38630a8cdf77f0f685f369e8 merged diff -r 3f8c7183ddac -r 40c9fb60de3c FSet.thy --- 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 *}) diff -r 3f8c7183ddac -r 40c9fb60de3c IntEx.thy --- 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"; *} diff -r 3f8c7183ddac -r 40c9fb60de3c LFex.thy --- 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: "\ty name kind. \P2 ty; P1 kind\ \ P1 (KPI ty name kind)" + and a2: "\id. P2 (TCONST id)" + and a3: "\ty trm. \P2 ty; P3 trm\ \ P2 (TAPP ty trm)" + and a4: "\ty1 name ty2. \P2 ty1; P2 ty2\ \ P2 (TPI ty1 name ty2)" + and a5: "\id. P3 (CONS id)" + and a6: "\name. P3 (VAR name)" + and a7: "\trm1 trm2. \P3 trm1; P3 trm2\ \ P3 (APP trm1 trm2)" + and a8: "\ty name trm. \P2 ty; P3 trm\ \ P3 (LAM ty name trm)" + shows "P1 mkind \ P2 mty \ P3 mtrm" +using a0 a1 a2 a3 a4 a5 a6 a7 a8 +*) + +lemma "\P1 TYP; + \ty name kind. \P2 ty; P1 kind\ \ P1 (KPI ty name kind); + \id. P2 (TCONST id); + \ty trm. \P2 ty; P3 trm\ \ P2 (TAPP ty trm); + \ty1 name ty2. \P2 ty1; P2 ty2\ \ P2 (TPI ty1 name ty2); + \id. P3 (CONS id); \name. P3 (VAR name); + \trm1 trm2. \P3 trm1; P3 trm2\ \ P3 (APP trm1 trm2); + \ty name trm. \P2 ty; P3 trm\ \ P3 (LAM ty name trm)\ + \ P1 mkind \ P2 mty \ 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 diff -r 3f8c7183ddac -r 40c9fb60de3c LamEx.thy --- 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 *} diff -r 3f8c7183ddac -r 40c9fb60de3c QuotMain.thy --- 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\) (Ball\) ----> (op =) (\) (\) *) - NDT ctxt "3" (rtac @{thm RES_FORALL_RSP}), + NDT ctxt "3" (rtac @{thm ball_rsp}), (* (R1 ===> R2) (Ball\) (Ball\) ----> \R1 x y\ \ R2 (Ball\x) (Ball\y) *) NDT ctxt "4" (ball_rsp_tac ctxt), (* (op =) (Bex\) (Bex\) ----> (op =) (\) (\) *) - NDT ctxt "5" (rtac @{thm RES_EXISTS_RSP}), + NDT ctxt "5" (rtac @{thm bex_rsp}), (* (R1 ===> R2) (Bex\) (Bex\) ----> \R1 x y\ \ R2 (Bex\x) (Bex\y) *) NDT ctxt "6" (bex_rsp_tac ctxt), @@ -946,7 +947,7 @@ (* R (\) (Rep (Abs \)) ----> R (\) (\) *) (* 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 $ \) (t' $ \) ----> 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) (\x. Rep2 (?f (Abs1 x))) \ ?f + - Rewriting with definitions from the argument defs + (Abs) OldConst (Rep Args) \ NewConst Args + - QUOTIENT_REL_REP: + Rel (Rep x) (Rep y) \ x = y + - FORALL_PRS (and the same for exists: EXISTS_PRS) + \x\Respects R. (abs ---> id) ?f \ \x. ?f + - applic_prs + Abs1 ((Abs2 --> Rep1) f (Rep2 args)) \ 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 diff -r 3f8c7183ddac -r 40c9fb60de3c QuotScript.thy --- 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 \ E (Rep (Abs r)) r" + assumes a: "QUOTIENT R Abs Rep" + shows "R r r \ 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 "(\x. f x) = (Rep1 ---> Abs2) (\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 \ bool" @@ -525,49 +536,29 @@ "((\y. \x. A x y) \ (\y. \x\P. B x y)) \ ((\x. \y. A x y) \ (\x\P. \y. B x y))" by auto - - -(* TODO: Add similar *) -lemma RES_FORALL_RSP: - shows "\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 "\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