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 *}