# HG changeset patch # User Christian Urban # Date 1259793090 -3600 # Node ID 2b7b349e470f8f9cc09f311c7c6f4c0daf9ea670 # Parent 508f3106b89ca7b0eaa12e99e187909dbf47b5cb deleted now obsolete argument rty everywhere diff -r 508f3106b89c -r 2b7b349e470f FSet.thy --- a/FSet.thy Wed Dec 02 23:11:50 2009 +0100 +++ b/FSet.thy Wed Dec 02 23:31:30 2009 +0100 @@ -300,12 +300,12 @@ 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 {* val consts = lookup_quot_consts defs *} -ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *} +ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] [quot] defs *} 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} rty [quot] [rel_refl] [trans2] 1 *}) +apply(tactic {* all_inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *}) apply(tactic {* clean_tac @{context} [quot] defs 1*}) done @@ -333,7 +333,7 @@ apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) done -ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *} +ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [quot] [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 *}) @@ -435,8 +435,8 @@ ML {* val defs = @{thms EMPTY2_def INSERT2_def} @ defs *} ML {* val quot = @{thms QUOTIENT_fset QUOTIENT_fset2} *} -ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty quot [rel_refl] [trans2] *} -ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty quot defs *} +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 defs *} 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 *}) @@ -471,7 +471,7 @@ ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *} -ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *} +ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] quot defs *} 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 508f3106b89c -r 2b7b349e470f IntEx.thy --- a/IntEx.thy Wed Dec 02 23:11:50 2009 +0100 +++ b/IntEx.thy Wed Dec 02 23:31:30 2009 +0100 @@ -140,10 +140,10 @@ ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *} ML {* val consts = lookup_quot_consts defs *} -ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *} +ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] [quot] defs *} -ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *} -ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *} +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] *} lemma "PLUS a b = PLUS b a" @@ -252,7 +252,7 @@ apply (rule allI) apply (rule allI) apply (rule impI) -apply (induct_tac xb yb rule:list_induct2) (* To finish I need to give it: arbitrary:xa ya *) +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]: diff -r 508f3106b89c -r 2b7b349e470f LFex.thy --- a/LFex.thy Wed Dec 02 23:11:50 2009 +0100 +++ b/LFex.thy Wed Dec 02 23:31:30 2009 +0100 @@ -267,7 +267,7 @@ apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) prefer 2 apply(tactic {* clean_tac @{context} quot defs 1 *}) -apply(tactic {* all_inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) +apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1*}) done (* Does not work: @@ -296,7 +296,7 @@ \ P1 mkind \ P2 mty \ P3 mtrm" apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *}) apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) -apply(tactic {* all_inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) +apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *}) apply(tactic {* clean_tac @{context} quot defs 1 *}) done diff -r 508f3106b89c -r 2b7b349e470f QuotMain.thy --- a/QuotMain.thy Wed Dec 02 23:11:50 2009 +0100 +++ b/QuotMain.thy Wed Dec 02 23:31:30 2009 +0100 @@ -990,7 +990,7 @@ *} ML {* -fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 = +fun inj_repabs_tac ctxt quot_thms 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\ *) @@ -1050,8 +1050,8 @@ *} ML {* -fun all_inj_repabs_tac ctxt rty quot_thms rel_refl trans2 = - REPEAT_ALL_NEW (inj_repabs_tac ctxt rty quot_thms rel_refl trans2) +fun all_inj_repabs_tac ctxt quot_thms rel_refl trans2 = + REPEAT_ALL_NEW (inj_repabs_tac ctxt quot_thms rel_refl trans2) *} section {* Cleaning of the theorem *} @@ -1276,7 +1276,8 @@ ML {* (* FIXME/TODO should only get as arguments the rthm like procedure_tac *) -fun lift_tac lthy rthm rel_eqv rty quot defs = + +fun lift_tac lthy rthm rel_eqv quot defs = ObjectLogic.full_atomize_tac THEN' gen_frees_tac lthy THEN' Subgoal.FOCUS (fn {context, concl, ...} => @@ -1291,7 +1292,7 @@ [rtac rule, RANGE [rtac rthm', regularize_tac lthy rel_eqv, - rtac thm THEN' all_inj_repabs_tac lthy rty quot rel_refl trans2, + rtac thm THEN' all_inj_repabs_tac lthy quot rel_refl trans2, clean_tac lthy quot defs]] end) lthy *}