# HG changeset patch # User Christian Urban <urbanc@in.tum.de> # Date 1260231943 -3600 # Node ID 51a4208162ed0b26d2b3cfc40353777b00183645 # Parent 018aabbffd0839d9e1b9cba62f3b2024fa726a7d added a thm list for ids diff -r 018aabbffd08 -r 51a4208162ed Quot/QuotMain.thy --- a/Quot/QuotMain.thy Tue Dec 08 01:00:21 2009 +0100 +++ b/Quot/QuotMain.thy Tue Dec 08 01:25:43 2009 +0100 @@ -147,8 +147,6 @@ (* Throws now an exception: *) (* declare [[map "option" = (bla, blu)]] *) - -(* identity quotient is not here as it has to be applied first *) lemmas [quotient_thm] = fun_quotient prod_quotient @@ -160,19 +158,17 @@ lemmas [quotient_equiv] = identity_equivp prod_equivp - (* definition of the quotient types *) (* FIXME: should be called quotient_typ.ML *) use "quotient.ML" - (* lifting of constants *) use "quotient_def.ML" section {* Simset setup *} -(* since HOL_basic_ss is too "big", we need to set up *) -(* our own minimal simpset *) +(* Since HOL_basic_ss is too "big" for us, *) +(* we set up our own minimal simpset. *) ML {* fun mk_minimal_ss ctxt = Simplifier.context ctxt empty_ss @@ -181,13 +177,10 @@ *} ML {* -(* TODO/FIXME not needed anymore? *) -fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) - fun OF1 thm1 thm2 = thm2 RS thm1 *} -section {* atomize *} +section {* Atomize Infrastructure *} lemma atomize_eqv[atomize]: shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" @@ -219,24 +212,20 @@ end *} -section {* infrastructure about id *} +section {* Infrastructure about id *} + +print_attributes (* TODO: think where should this be *) lemma prod_fun_id: "prod_fun id id \<equiv> id" by (rule eq_reflection) (simp add: prod_fun_def) -(* FIXME: make it a list and add map_id to it *) -lemmas id_simps = +lemmas [id_simps] = fun_map_id[THEN eq_reflection] id_apply[THEN eq_reflection] id_def[THEN eq_reflection,symmetric] prod_fun_id -ML {* -fun simp_ids thm = - MetaSimplifier.rewrite_rule @{thms id_simps} thm -*} - section {* Debugging infrastructure for testing tactics *} ML {* @@ -1008,7 +997,7 @@ val _ = tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te))); val ti = (let - val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te + val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) in Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts @@ -1017,7 +1006,7 @@ val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm) val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te in - MetaSimplifier.rewrite_rule @{thms id_simps} td + MetaSimplifier.rewrite_rule (id_simps_get ctxt) td end); val _ = if not (Term.is_Const a2 andalso fst (dest_Const a2) = @{const_name "id"}) then (tracing "lambda_prs"; @@ -1045,8 +1034,8 @@ (* 2. folding of definitions: (rep ---> abs) oldConst == newconst *) (* and simplification with *) thm all_prs ex_prs -(* 3. simplification with *) -thm fun_map.simps id_simps Quotient_abs_rep Quotient_rel_rep +(* 3. simplification with id_simps and *) +thm fun_map.simps Quotient_abs_rep Quotient_rel_rep (* 4. Test for refl *) ML {* @@ -1056,8 +1045,8 @@ val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) (* FIXME: shouldn't the definitions already be varified? *) val thms1 = @{thms all_prs ex_prs} @ defs - val thms2 = @{thms eq_reflection[OF fun_map.simps]} - @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} + val thms2 = @{thms eq_reflection[OF fun_map.simps]} @ (id_simps_get lthy) + @ @{thms Quotient_abs_rep Quotient_rel_rep} fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver in EVERY' [lambda_prs_tac lthy, diff -r 018aabbffd08 -r 51a4208162ed Quot/quotient_info.ML --- a/Quot/quotient_info.ML Tue Dec 08 01:00:21 2009 +0100 +++ b/Quot/quotient_info.ML Tue Dec 08 01:25:43 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 id_simps_get: Proof.context -> thm list val quotient_rules_get: Proof.context -> thm list val quotient_rules_add: attribute end; @@ -174,6 +175,9 @@ OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants" OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of))) +(* FIXME/TODO: check the various lemmas conform *) +(* with the required shape *) + (* equivalence relation theorems *) structure EquivRules = Named_Thms (val name = "quotient_equiv" @@ -189,6 +193,13 @@ val rsp_rules_get = RspRules.get +(* respectfulness theorems *) +structure IdSimps = Named_Thms + (val name = "id_simps" + val description = "Identity simp rules for maps.") + +val id_simps_get = IdSimps.get + (* quotient theorems *) structure QuotientRules = Named_Thms (val name = "quotient_thm" @@ -201,6 +212,7 @@ val _ = Context.>> (Context.map_theory (EquivRules.setup #> RspRules.setup #> + IdSimps.setup #> QuotientRules.setup)) end; (* structure *)