# HG changeset patch # User Cezary Kaliszyk # Date 1259915127 -3600 # Node ID 6b3be083229c512f6c2f875483bf7f853024f35c # Parent eed5d55ea9a69c65cb23c49802c457e9652a72b8# Parent 28bb34eeedc5ce593f180772135a3e3225eb33ce The big merge; probably non-functional. diff -r eed5d55ea9a6 -r 6b3be083229c FIXME-TODO --- 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 diff -r eed5d55ea9a6 -r 6b3be083229c FSet.thy --- 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 = []) \ (\a. \ Y. (~(a memb Y) \ (X \ 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 \ ===> 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 \ ===> op =) card1 card1" by (simp add: card1_rsp) -lemma cons_rsp[quot_rsp]: +lemma cons_rsp[quotient_rsp]: fixes z assumes a: "xs \ ys" shows "(z # xs) \ (z # ys)" using a by (rule list_eq.intros(5)) -lemma ho_cons_rsp[quot_rsp]: +lemma ho_cons_rsp[quotient_rsp]: "(op = ===> op \ ===> op \) 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 \ ===> op \ ===> op \) 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 \ ===> op \) map map" by (simp add: map_rsp) @@ -277,7 +274,7 @@ "(map f (a @ b)) \ (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 \ ===> 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 \ 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) \ (\e t. P x t \ P x (INSERT e t)) \ P x l" apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) done @@ -431,8 +431,8 @@ "INSERT2 \ 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) \ (\e t. P x t \ P x (INSERT e t)) \ P x l" apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) @@ -453,20 +453,20 @@ "fset_case \ 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 \ ===> op =) ===> op \ ===> 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 \ ===> op =) ===> op \ ===> 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 *}) diff -r eed5d55ea9a6 -r 6b3be083229c IntEx.thy --- 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 \ ===> LIST_REL op \ ===> LIST_REL op \) op # op #" by simp (* I believe it's true. *) -lemma foldl_rsp[quot_rsp]: +lemma foldl_rsp[quotient_rsp]: "((op \ ===> op \ ===> op \) ===> op \ ===> LIST_REL op \ ===> op \) 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: - "\QUOTIENT R absf repf; f = g\ \ Ball (Respects R) ((absf ---> id) f) = All g" -apply(drule all_prs) -apply(simp) -done - -lemma test: - "\QUOTIENT R1 Abs1 Rep1; QUOTIENT R2 Abs2 Rep2; - (\x. Rep2 (f (Abs1 x))) = lhs \ \ (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) \ 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 diff -r eed5d55ea9a6 -r 6b3be083229c LFex.thy --- 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 \ (perm::'x prm \ trm \ 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 \ op \" sorry -lemma perm_ty_rsp[quot_rsp]: +lemma perm_ty_rsp[quotient_rsp]: "(op = ===> aty ===> aty) op \ op \" sorry -lemma perm_trm_rsp[quot_rsp]: +lemma perm_trm_rsp[quotient_rsp]: "(op = ===> atrm ===> atrm) op \ op \" 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 @@ \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 {* 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 diff -r eed5d55ea9a6 -r 6b3be083229c LamEx.thy --- 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 \ op \" 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)]\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 \ 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\('x \ 'x) list) \ Var a = Var (pi \ a)" apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *}) @@ -312,39 +312,32 @@ "\t = [(a, b)] \ s; a \ [b].s\ \ 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 diff -r eed5d55ea9a6 -r 6b3be083229c QuotList.thy --- 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 \ LIST_REL R xs ys)" lemma LIST_REL_EQ: - shows "LIST_REL (op =) = (op =)" + shows "LIST_REL (op =) \ (op =)" unfolding expand_fun_eq apply(rule allI)+ apply(induct_tac x xa rule: list_induct2') diff -r eed5d55ea9a6 -r 6b3be083229c QuotMain.thy --- 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) ----> \R a c; R b d\ *) @@ -933,11 +931,11 @@ (* R (\) (Rep (Abs \)) ----> R (\) (\) *) (* 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 $ \) (t' $ \) ----> 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 $ \) (t' $ \) ----> 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 =) \ (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) (\x. Rep2 (f (Abs1 x))) ----> f *) (* \x\Respects R. (abs ---> id) f ----> \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 *} diff -r eed5d55ea9a6 -r 6b3be083229c QuotScript.thy --- 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 \ FUN_REL E1 E2" lemma FUN_REL_EQ: - "(op =) ===> (op =) = (op =)" + "(op =) ===> (op =) \ (op =)" by (simp add: expand_fun_eq) lemma FUN_QUOTIENT: diff -r eed5d55ea9a6 -r 6b3be083229c quotient_info.ML --- 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