# HG changeset patch # User Christian Urban # Date 1260289800 -3600 # Node ID 520a4084d064450c18ec3359773ada0fc4fd4d24 # Parent 2e51e13158391de70d0fdd0be5a811da1a90a3d5 changed names of attributes diff -r 2e51e1315839 -r 520a4084d064 Quot/Examples/FSet.thy --- a/Quot/Examples/FSet.thy Tue Dec 08 16:36:01 2009 +0100 +++ b/Quot/Examples/FSet.thy Tue Dec 08 17:30:00 2009 +0100 @@ -177,7 +177,7 @@ shows "(z memb x) = (z memb y)" using a by induct auto -lemma ho_memb_rsp[quotient_rsp]: +lemma ho_memb_rsp[quot_respect]: "(op = ===> (op \ ===> op =)) (op memb) (op memb)" by (simp add: memb_rsp) @@ -187,17 +187,17 @@ shows "card1 a = card1 b" using e by induct (simp_all add:memb_rsp) -lemma ho_card1_rsp[quotient_rsp]: +lemma ho_card1_rsp[quot_respect]: "(op \ ===> op =) card1 card1" by (simp add: card1_rsp) -lemma cons_rsp[quotient_rsp]: +lemma cons_rsp[quot_respect]: fixes z assumes a: "xs \ ys" shows "(z # xs) \ (z # ys)" using a by (rule list_eq.intros(5)) -lemma ho_cons_rsp[quotient_rsp]: +lemma ho_cons_rsp[quot_respect]: "(op = ===> op \ ===> op \) op # op #" by (simp add: cons_rsp) @@ -254,7 +254,7 @@ apply (rule append_sym_rsp) done -lemma ho_append_rsp[quotient_rsp]: +lemma ho_append_rsp[quot_respect]: "(op \ ===> op \ ===> op \) op @ op @" by (simp add: append_rsp) @@ -266,7 +266,7 @@ apply(auto intro: list_eq.intros) done -lemma ho_map_rsp[quotient_rsp]: +lemma ho_map_rsp[quot_respect]: "(op = ===> op \ ===> op \) map map" by (simp add: map_rsp) @@ -274,7 +274,7 @@ "(map f (a @ b)) \ (map f a) @ (map f b)" by simp (rule list_eq_refl) -lemma ho_fold_rsp[quotient_rsp]: +lemma ho_fold_rsp[quot_respect]: "(op = ===> op = ===> op = ===> op \ ===> op =) fold1 fold1" apply (auto) apply (case_tac "rsp_fold x") @@ -286,7 +286,7 @@ apply (auto simp add: memb_rsp rsp_fold_def) done -lemma list_equiv_rsp[quotient_rsp]: +lemma list_equiv_rsp[quot_respect]: shows "(op \ ===> op \ ===> op =) op \ op \" by (auto intro: list_eq.intros) @@ -355,8 +355,6 @@ apply (assumption) done -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 @{context} @{thm list_induct_part} 1 *}) done @@ -402,14 +400,14 @@ "fset_case \ list_case" (* Probably not true without additional assumptions about the function *) -lemma list_rec_rsp[quotient_rsp]: +lemma list_rec_rsp[quot_respect]: "(op = ===> (op = ===> op \ ===> op =) ===> op \ ===> op =) list_rec list_rec" apply (auto) apply (erule_tac list_eq.induct) apply (simp_all) sorry -lemma list_case_rsp[quotient_rsp]: +lemma list_case_rsp[quot_respect]: "(op = ===> (op = ===> op \ ===> op =) ===> op \ ===> op =) list_case list_case" apply (auto) sorry diff -r 2e51e1315839 -r 520a4084d064 Quot/Examples/IntEx.thy --- a/Quot/Examples/IntEx.thy Tue Dec 08 16:36:01 2009 +0100 +++ b/Quot/Examples/IntEx.thy Tue Dec 08 17:30:00 2009 +0100 @@ -12,9 +12,9 @@ apply(auto simp add: mem_def expand_fun_eq) done -thm quotient_equiv +thm quot_equiv -thm quotient_thm +thm quot_thm thm my_int_equivp @@ -132,7 +132,7 @@ apply(auto) done -lemma plus_rsp[quotient_rsp]: +lemma plus_rsp[quot_respect]: shows "(intrel ===> intrel ===> intrel) my_plus my_plus" by (simp) @@ -171,8 +171,8 @@ apply(tactic {* procedure_tac @{context} @{thm test3} 1 *}) apply(rule impI) apply(rule plus_rsp) -apply(tactic {* all_inj_repabs_tac @{context} 1*}) -apply(tactic {* clean_tac @{context} 1 *}) +apply(injection) +apply(cleaning) done @@ -203,9 +203,7 @@ done lemma "foldl PLUS x [] = x" -apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) -apply(tactic {* regularize_tac @{context} 1 *}) -apply(tactic {* all_inj_repabs_tac @{context} 1*}) +apply(lifting rule: ho_tst) apply(tactic {* clean_tac @{context} 1 *}) apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int]) done @@ -345,14 +343,10 @@ done lemma "map (\x. PLUS x ZERO) l = l" -apply(tactic {* procedure_tac @{context} @{thm lam_tst4} 1 *}) -apply(tactic {* regularize_tac @{context} 1 *}) -apply(tactic {* all_inj_repabs_tac @{context} 1*}) -apply(tactic {* clean_tac @{context} 1*}) +apply(lifting rule: lam_tst4) +apply(cleaning) apply(simp only: babs_prs[OF Quotient_my_int Quotient_my_int]) -apply(simp only: map_prs[OF Quotient_my_int Quotient_my_int]) -apply(tactic {* lambda_prs_tac @{context} 1 *}) -apply(rule refl) +apply(simp only: map_prs[OF Quotient_my_int Quotient_my_int, symmetric]) done end diff -r 2e51e1315839 -r 520a4084d064 Quot/Examples/IntEx2.thy --- a/Quot/Examples/IntEx2.thy Tue Dec 08 16:36:01 2009 +0100 +++ b/Quot/Examples/IntEx2.thy Tue Dec 08 17:30:00 2009 +0100 @@ -107,21 +107,21 @@ thm add_assoc -lemma plus_raw_rsp[quotient_rsp]: +lemma plus_raw_rsp[quot_respect]: shows "(op \ ===> op \ ===> op \) plus_raw plus_raw" by auto -lemma minus_raw_rsp[quotient_rsp]: +lemma minus_raw_rsp[quot_respect]: shows "(op \ ===> op \) minus_raw minus_raw" by auto -lemma mult_raw_rsp[quotient_rsp]: +lemma mult_raw_rsp[quot_respect]: shows "(op \ ===> op \ ===> op \) mult_raw mult_raw" apply(auto) apply(simp add: algebra_simps) sorry -lemma le_raw_rsp[quotient_rsp]: +lemma le_raw_rsp[quot_respect]: shows "(op \ ===> op \ ===> op =) le_raw le_raw" by auto diff -r 2e51e1315839 -r 520a4084d064 Quot/Examples/LFex.thy --- a/Quot/Examples/LFex.thy Tue Dec 08 16:36:01 2009 +0100 +++ b/Quot/Examples/LFex.thy Tue Dec 08 17:30:00 2009 +0100 @@ -183,35 +183,35 @@ end (* TODO/FIXME: Think whether these RSP theorems are true. *) -lemma kpi_rsp[quotient_rsp]: +lemma kpi_rsp[quot_respect]: "(aty ===> op = ===> akind ===> akind) KPi KPi" sorry -lemma tconst_rsp[quotient_rsp]: +lemma tconst_rsp[quot_respect]: "(op = ===> aty) TConst TConst" sorry -lemma tapp_rsp[quotient_rsp]: +lemma tapp_rsp[quot_respect]: "(aty ===> atrm ===> aty) TApp TApp" sorry -lemma tpi_rsp[quotient_rsp]: +lemma tpi_rsp[quot_respect]: "(aty ===> op = ===> aty ===> aty) TPi TPi" sorry -lemma var_rsp[quotient_rsp]: +lemma var_rsp[quot_respect]: "(op = ===> atrm) Var Var" sorry -lemma app_rsp[quotient_rsp]: +lemma app_rsp[quot_respect]: "(atrm ===> atrm ===> atrm) App App" sorry -lemma const_rsp[quotient_rsp]: +lemma const_rsp[quot_respect]: "(op = ===> atrm) Const Const" sorry -lemma lam_rsp[quotient_rsp]: +lemma lam_rsp[quot_respect]: "(aty ===> op = ===> atrm ===> atrm) Lam Lam" sorry -lemma perm_kind_rsp[quotient_rsp]: +lemma perm_kind_rsp[quot_respect]: "(op = ===> akind ===> akind) op \ op \" sorry -lemma perm_ty_rsp[quotient_rsp]: +lemma perm_ty_rsp[quot_respect]: "(op = ===> aty ===> aty) op \ op \" sorry -lemma perm_trm_rsp[quotient_rsp]: +lemma perm_trm_rsp[quot_respect]: "(op = ===> atrm ===> atrm) op \ op \" sorry -lemma fv_ty_rsp[quotient_rsp]: +lemma fv_ty_rsp[quot_respect]: "(aty ===> op =) fv_ty fv_ty" sorry -lemma fv_kind_rsp[quotient_rsp]: +lemma fv_kind_rsp[quot_respect]: "(akind ===> op =) fv_kind fv_kind" sorry -lemma fv_trm_rsp[quotient_rsp]: +lemma fv_trm_rsp[quot_respect]: "(atrm ===> op =) fv_trm fv_trm" sorry diff -r 2e51e1315839 -r 520a4084d064 Quot/Examples/LamEx.thy --- a/Quot/Examples/LamEx.thy Tue Dec 08 16:36:01 2009 +0100 +++ b/Quot/Examples/LamEx.thy Tue Dec 08 17:30:00 2009 +0100 @@ -128,7 +128,7 @@ unfolding fresh_def supp_def sorry -lemma perm_rsp[quotient_rsp]: +lemma perm_rsp[quot_respect]: "(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[quotient_rsp]: +lemma rVar_rsp[quot_respect]: "(op = ===> alpha) rVar rVar" by (auto intro:a1) -lemma rApp_rsp[quotient_rsp]: "(alpha ===> alpha ===> alpha) rApp rApp" +lemma rApp_rsp[quot_respect]: "(alpha ===> alpha ===> alpha) rApp rApp" by (auto intro:a2) -lemma rLam_rsp[quotient_rsp]: "(op = ===> alpha ===> alpha) rLam rLam" +lemma rLam_rsp[quot_respect]: "(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[quotient_rsp]: "(alpha ===> op =) rfv rfv" +lemma rfv_rsp[quot_respect]: "(alpha ===> op =) rfv rfv" sorry lemma rvar_inject: "rVar a \ rVar b = (a = b)" diff -r 2e51e1315839 -r 520a4084d064 Quot/QuotList.thy --- a/Quot/QuotList.thy Tue Dec 08 16:36:01 2009 +0100 +++ b/Quot/QuotList.thy Tue Dec 08 17:30:00 2009 +0100 @@ -12,7 +12,7 @@ declare [[map list = (map, list_rel)]] -lemma list_equivp[quotient_equiv]: +lemma list_equivp[quot_equiv]: assumes a: "equivp R" shows "equivp (list_rel R)" unfolding equivp_def @@ -40,7 +40,7 @@ apply(metis) done -lemma list_quotient[quotient_thm]: +lemma list_quotient[quot_thm]: assumes q: "Quotient R Abs Rep" shows "Quotient (list_rel R) (map Abs) (map Rep)" unfolding Quotient_def @@ -72,7 +72,7 @@ shows "(map Abs) ((Rep h) # (map Rep t)) = h # t" by (induct t) (simp_all add: Quotient_abs_rep[OF q]) -lemma cons_rsp[quotient_rsp]: +lemma cons_rsp[quot_respect]: assumes q: "Quotient R Abs Rep" shows "(R ===> list_rel R ===> list_rel R) op # op #" by (auto) @@ -82,7 +82,7 @@ shows "map Abs [] \ []" by (simp) -lemma nil_rsp[quotient_rsp]: +lemma nil_rsp[quot_respect]: assumes q: "Quotient R Abs Rep" shows "list_rel R [] []" by simp @@ -93,7 +93,7 @@ shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l" by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) -lemma map_rsp[quotient_rsp]: +lemma map_rsp[quot_respect]: assumes q1: "Quotient R1 Abs1 Rep1" and q2: "Quotient R2 Abs2 Rep2" shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map" @@ -131,7 +131,7 @@ induct doesn't accept 'rule'. that's why the proof uses manual generalisation and needs assumptions both in conclusion for induction and in assumptions. *) -lemma foldl_rsp[quotient_rsp]: +lemma foldl_rsp[quot_respect]: assumes q1: "Quotient R1 Abs1 Rep1" and q2: "Quotient R2 Abs2 Rep2" shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl" diff -r 2e51e1315839 -r 520a4084d064 Quot/QuotMain.thy --- a/Quot/QuotMain.thy Tue Dec 08 16:36:01 2009 +0100 +++ b/Quot/QuotMain.thy Tue Dec 08 17:30:00 2009 +0100 @@ -148,15 +148,15 @@ (* Throws now an exception: *) (* declare [[map "option" = (bla, blu)]] *) -lemmas [quotient_thm] = +lemmas [quot_thm] = fun_quotient prod_quotient -lemmas [quotient_rsp] = +lemmas [quot_respect] = quot_rel_rsp pair_rsp (* fun_map is not here since equivp is not true *) (* TODO: option, ... *) -lemmas [quotient_equiv] = +lemmas [quot_equiv] = identity_equivp prod_equivp (* definition of the quotient types *) @@ -1063,6 +1063,7 @@ EVERY' [lambda_prs_tac lthy, simp_tac (simps thms1), simp_tac (simps thms2), + lambda_prs_tac lthy, TRY o rtac refl] end *} @@ -1185,6 +1186,7 @@ (clean_tac ctxt, "Cleaning proof failed.")] *} +(* methods / interface *) ML {* val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thm diff -r 2e51e1315839 -r 520a4084d064 Quot/quotient_info.ML --- a/Quot/quotient_info.ML Tue Dec 08 16:36:01 2009 +0100 +++ b/Quot/quotient_info.ML Tue Dec 08 17:30:00 2009 +0100 @@ -26,6 +26,7 @@ val equiv_rules_get: Proof.context -> thm list val equiv_rules_add: attribute val rsp_rules_get: Proof.context -> thm list + val prs_rules_get: Proof.context -> thm list val id_simps_get: Proof.context -> thm list val quotient_rules_get: Proof.context -> thm list val quotient_rules_add: attribute @@ -180,7 +181,7 @@ (* equivalence relation theorems *) structure EquivRules = Named_Thms - (val name = "quotient_equiv" + (val name = "quot_equiv" val description = "Equivalence relation theorems.") val equiv_rules_get = EquivRules.get @@ -188,11 +189,18 @@ (* respectfulness theorems *) structure RspRules = Named_Thms - (val name = "quotient_rsp" + (val name = "quot_respect" val description = "Respectfulness theorems.") val rsp_rules_get = RspRules.get +(* preservation theorems *) +structure PrsRules = Named_Thms + (val name = "quot_preserve" + val description = "Respectfulness theorems.") + +val prs_rules_get = PrsRules.get + (* respectfulness theorems *) structure IdSimps = Named_Thms (val name = "id_simps" @@ -202,7 +210,7 @@ (* quotient theorems *) structure QuotientRules = Named_Thms - (val name = "quotient_thm" + (val name = "quot_thm" val description = "Quotient theorems.") val quotient_rules_get = QuotientRules.get