# HG changeset patch # User wenzelm # Date 1164402317 -3600 # Node ID 095f4963beed96be5a672e474386d0376ece30e8 # Parent 63c73f461eec7a093b54baa353db3b1bd3f0ee73 simultaneous fact morphism; diff -r 63c73f461eec -r 095f4963beed src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Fri Nov 24 22:05:16 2006 +0100 +++ b/src/Pure/Isar/element.ML Fri Nov 24 22:05:17 2006 +0100 @@ -114,7 +114,7 @@ var = Morphism.var phi, typ = Morphism.typ phi, term = Morphism.term phi, - fact = map (Morphism.thm phi), + fact = Morphism.fact phi, attrib = Args.morph_values phi}; @@ -327,13 +327,10 @@ end; fun hyps_rule rule th = - let - val cterm_rule = Drule.mk_term #> rule #> Drule.dest_term; - val {hyps, ...} = Thm.crep_thm th; - in + let val {hyps, ...} = Thm.crep_thm th in Drule.implies_elim_list (rule (Drule.implies_intr_list hyps th)) - (map (Thm.assume o cterm_rule) hyps) + (map (Thm.assume o Drule.cterm_rule rule) hyps) end; @@ -372,7 +369,7 @@ end; fun rename_morphism ren = Morphism.morphism - {name = I, var = rename_var ren, typ = I, term = rename_term ren, thm = rename_thm ren}; + {name = I, var = rename_var ren, typ = I, term = rename_term ren, fact = map (rename_thm ren)}; (* instantiate types *) @@ -398,7 +395,7 @@ in if null subst then th else th |> hyps_rule (instantiate_tfrees thy subst) end; fun instT_morphism thy env = Morphism.morphism - {name = I, var = I, typ = instT_type env, term = instT_term env, thm = instT_thm thy env}; + {name = I, var = I, typ = instT_type env, term = instT_term env, fact = map (instT_thm thy env)}; (* instantiate types and terms *) @@ -441,7 +438,8 @@ end; fun inst_morphism thy envs = Morphism.morphism - {name = I, var = I, typ = instT_type (#1 envs), term = inst_term envs, thm = inst_thm thy envs}; + {name = I, var = I, typ = instT_type (#1 envs), term = inst_term envs, + fact = map (inst_thm thy envs)}; (* satisfy hypotheses *) @@ -469,13 +467,13 @@ val thy = ProofContext.theory_of inner; val maxidx = fold (fn ((_, atts), bs) => maxidx_atts atts #> fold (maxidx_atts o #2) bs) facts ~1; - val exp_thm = Thm.adjust_maxidx_thm maxidx #> - singleton ((if std then ProofContext.export_standard else ProofContext.export) inner outer); - val exp_term = Drule.term_rule thy exp_thm; - val exp_typ = Logic.mk_type #> exp_term #> Logic.dest_type; - val exp_morphism = - Morphism.morphism {name = I, var = I, typ = exp_typ, term = exp_term, thm = exp_thm}; - val Notes (_, facts') = morph_ctxt exp_morphism (Notes ("", facts)); + val exp_fact = map (Thm.adjust_maxidx_thm maxidx) #> + ((if std then ProofContext.export_standard else ProofContext.export) inner outer); + val exp_term = Drule.term_rule thy (singleton exp_fact); + val exp_typ = Logic.type_map exp_term; + val morphism = + Morphism.morphism {name = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact}; + val Notes (_, facts') = morph_ctxt morphism (Notes ("", facts)); in facts' end; in diff -r 63c73f461eec -r 095f4963beed src/Pure/morphism.ML --- a/src/Pure/morphism.ML Fri Nov 24 22:05:16 2006 +0100 +++ b/src/Pure/morphism.ML Fri Nov 24 22:05:17 2006 +0100 @@ -20,17 +20,19 @@ val name: morphism -> string -> string val typ: morphism -> typ -> typ val term: morphism -> term -> term + val fact: morphism -> thm list -> thm list val thm: morphism -> thm -> thm val morphism: {name: string -> string, var: string * mixfix -> string * mixfix, typ: typ -> typ, term: term -> term, - thm: thm -> thm} -> morphism + fact: thm list -> thm list} -> morphism val name_morphism: (string -> string) -> morphism val var_morphism: (string * mixfix -> string * mixfix) -> morphism val typ_morphism: (typ -> typ) -> morphism val term_morphism: (term -> term) -> morphism + val fact_morphism: (thm list -> thm list) -> morphism val thm_morphism: (thm -> thm) -> morphism val identity: morphism val comp: morphism -> morphism -> morphism @@ -44,29 +46,31 @@ var: string * mixfix -> string * mixfix, typ: typ -> typ, term: term -> term, - thm: thm -> thm}; + fact: thm list -> thm list}; fun name (Morphism {name, ...}) = name; fun var (Morphism {var, ...}) = var; fun typ (Morphism {typ, ...}) = typ; fun term (Morphism {term, ...}) = term; -fun thm (Morphism {thm, ...}) = thm; +fun fact (Morphism {fact, ...}) = fact; +val thm = singleton o fact; val morphism = Morphism; -fun name_morphism name = morphism {name = name, var = I, typ = I, term = I, thm = I}; -fun var_morphism var = morphism {name = I, var = var, typ = I, term = I, thm = I}; -fun typ_morphism typ = morphism {name = I, var = I, typ = typ, term = I, thm = I}; -fun term_morphism term = morphism {name = I, var = I, typ = I, term = term, thm = I}; -fun thm_morphism thm = morphism {name = I, var = I, typ = I, term = I, thm = thm}; +fun name_morphism name = morphism {name = name, var = I, typ = I, term = I, fact = I}; +fun var_morphism var = morphism {name = I, var = var, typ = I, term = I, fact = I}; +fun typ_morphism typ = morphism {name = I, var = I, typ = typ, term = I, fact = I}; +fun term_morphism term = morphism {name = I, var = I, typ = I, term = term, fact = I}; +fun fact_morphism fact = morphism {name = I, var = I, typ = I, term = I, fact = fact}; +fun thm_morphism thm = morphism {name = I, var = I, typ = I, term = I, fact = map thm}; -val identity = morphism {name = I, var = I, typ = I, term = I, thm = I}; +val identity = morphism {name = I, var = I, typ = I, term = I, fact = I}; fun comp - (Morphism {name = name1, var = var1, typ = typ1, term = term1, thm = thm1}) - (Morphism {name = name2, var = var2, typ = typ2, term = term2, thm = thm2}) = + (Morphism {name = name1, var = var1, typ = typ1, term = term1, fact = fact1}) + (Morphism {name = name2, var = var2, typ = typ2, term = term2, fact = fact2}) = morphism {name = name1 o name2, var = var1 o var2, - typ = typ1 o typ2, term = term1 o term2, thm = thm1 o thm2}; + typ = typ1 o typ2, term = term1 o term2, fact = fact1 o fact2}; fun phi1 $> phi2 = comp phi2 phi1;