# HG changeset patch # User ballarin # Date 1227817534 -3600 # Node ID 530c7d28a96232fb94964c30fcd2385842e9a632 # Parent 3d166f1bd73345c24991cfc918d60a0985987220 Proper treatment of expressions with free arguments. diff -r 3d166f1bd733 -r 530c7d28a962 src/FOL/ex/NewLocaleTest.thy --- a/src/FOL/ex/NewLocaleTest.thy Thu Nov 27 21:25:16 2008 +0100 +++ b/src/FOL/ex/NewLocaleTest.thy Thu Nov 27 21:25:34 2008 +0100 @@ -216,4 +216,47 @@ print_locale! rgrp print_locale! lgrp + +(* locale with many parameters --- + interpretations generate alternating group A5 *) + +locale A5 = + fixes A and B and C and D and E + assumes eq: "A <-> B <-> C <-> D <-> E" + +sublocale A5 < 1: A5 _ _ D E C +print_facts + using eq apply (blast intro: A5.intro) done + +sublocale A5 < 2: A5 C _ E _ A +print_facts + using eq apply (blast intro: A5.intro) done + +sublocale A5 < 3: A5 B C A _ _ +print_facts + using eq apply (blast intro: A5.intro) done + +(* Any even permutation of parameters is subsumed by the above. *) + +print_locale! A5 + + +(* Free arguments of instance *) + +locale trivial = + fixes P and Q :: o + assumes Q: "P <-> P <-> Q" +begin + +lemma Q_triv: "Q" using Q by fast + end + +sublocale trivial < x: trivial x _ + apply (intro trivial.intro) using Q by fast + +print_locale! trivial + +context trivial begin thm x.Q [where ?x = True] end + +end diff -r 3d166f1bd733 -r 530c7d28a962 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Thu Nov 27 21:25:16 2008 +0100 +++ b/src/Pure/Isar/expression.ML Thu Nov 27 21:25:34 2008 +0100 @@ -12,7 +12,7 @@ type expression = string expr * (Name.binding * string option * mixfix) list; type expression_i = term expr * (Name.binding * typ option * mixfix) list; - (* Processing of locale statements *) + (* Processing of context statements *) val read_statement: Element.context list -> (string * string list) list list -> Proof.context -> (term * term list) list list * Proof.context; val cert_statement: Element.context_i list -> (term * term list) list list -> @@ -499,7 +499,7 @@ - Facts unchanged *) - in ((parms, fors', deps, elems', concl), text) end + in ((fors', deps, elems', concl), (parms, text)) end in @@ -512,41 +512,85 @@ end; -(* full context statements: import + elements + conclusion *) +(* Context statement: elements + conclusion *) local -fun prep_context_statement prep_full_context_statement activate_elems - strict do_close imprt elements raw_concl context = +fun prep_statement prep activate raw_elems raw_concl context = + let + val ((_, _, elems, concl), _) = prep true false context ([], []) raw_elems raw_concl; + val (_, context') = activate elems (ProofContext.set_stmt true context); + in (concl, context') end; + +in + +fun read_statement x = prep_statement read_full_context_statement Element.activate x; +fun cert_statement x = prep_statement cert_full_context_statement Element.activate_i x; + +end; + + +(* Locale declaration: import + elements *) + +local + +fun prep_declaration prep activate raw_import raw_elems context = let val thy = ProofContext.theory_of context; - val ((parms, fixed, deps, elems, concl), (spec, (_, _, defs))) = - prep_full_context_statement strict do_close context imprt elements raw_concl; - - val (_, ctxt0) = ProofContext.add_fixes_i fixed context; - val (_, ctxt) = fold (NewLocale.activate_facts thy) deps (NewLocale.empty, ctxt0); - val ((elems', _), ctxt') = activate_elems elems (ProofContext.set_stmt true ctxt); - in - (((fixed, deps), (ctxt', elems'), (parms, spec, defs)), concl) - end; - -fun prep_statement prep_ctxt elems concl ctxt = - let - val (((_, (ctxt', _), _)), concl) = prep_ctxt true false ([], []) elems concl ctxt - in (concl, ctxt') end; + val ((fixed, deps, elems, _), (parms, (spec, (_, _, defs)))) = + prep false true context raw_import raw_elems []; + (* Declare parameters and imported facts *) + val context' = context |> + ProofContext.add_fixes_i fixed |> snd |> + pair NewLocale.empty |> fold (NewLocale.activate_facts thy) deps |> snd; + val ((elems', _), _) = activate elems (ProofContext.set_stmt true context'); + in ((fixed, deps, elems'), (parms, spec, defs)) end; in -fun read_statement body concl ctxt = - prep_statement (prep_context_statement read_full_context_statement Element.activate) body concl ctxt; -fun cert_statement body concl ctxt = - prep_statement (prep_context_statement cert_full_context_statement Element.activate_i) body concl ctxt; +fun read_declaration x = prep_declaration read_full_context_statement Element.activate x; +fun cert_declaration x = prep_declaration cert_full_context_statement Element.activate_i x; + +end; + + +(* Locale expression to set up a goal *) + +local + +fun props_of thy (name, morph) = + let + val (asm, defs) = NewLocale.specification_of thy name; + in + (case asm of NONE => defs | SOME asm => asm :: defs) |> map (Morphism.term morph) + end; + +fun prep_goal_expression prep expression context = + let + val thy = ProofContext.theory_of context; -fun read_context strict imprt body ctxt = - #1 (prep_context_statement read_full_context_statement Element.activate strict true imprt body [] ctxt); -fun cert_context strict imprt body ctxt = - #1 (prep_context_statement cert_full_context_statement Element.activate_i strict true imprt body [] ctxt); + val ((fixed, deps, _, _), _) = prep true true context expression [] []; + (* proof obligations *) + val propss = map (props_of thy) deps; + + val goal_ctxt = context |> + ProofContext.add_fixes_i fixed |> snd |> + (fold o fold) Variable.auto_fixes propss; + + val export = Variable.export_morphism goal_ctxt context; + val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export; +(* val exp_term = TermSubst.zero_var_indexes o Morphism.term export; *) + val exp_term = Drule.term_rule thy (singleton exp_fact); + val exp_typ = Logic.type_map exp_term; + val export' = + Morphism.morphism {name = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact}; + in ((propss, deps, export'), goal_ctxt) end; + +in + +fun read_goal_expression x = prep_goal_expression read_full_context_statement x; +fun cert_goal_expression x = prep_goal_expression cert_full_context_statement x; end; @@ -581,7 +625,7 @@ Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args) else raise Match); -(* CB: define one predicate including its intro rule and axioms +(* define one predicate including its intro rule and axioms - bname: predicate name - parms: locale parameters - defs: thms representing substitutions from defines elements @@ -694,7 +738,7 @@ end | defines_to_notes _ e defns = (e, defns); -fun gen_add_locale prep_context +fun gen_add_locale prep_decl bname predicate_name raw_imprt raw_body thy = let val thy_ctxt = ProofContext.init thy; @@ -702,8 +746,8 @@ val _ = NewLocale.test_locale thy name andalso error ("Duplicate definition of locale " ^ quote name); - val ((fixed, deps), (_, body_elems), text as (parms, ((_, exts'), _), defs)) = - prep_context false raw_imprt raw_body thy_ctxt; + val ((fixed, deps, body_elems), text as (parms, ((_, exts'), _), defs)) = + prep_decl raw_imprt raw_body thy_ctxt; val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') = define_preds predicate_name text thy; @@ -732,8 +776,8 @@ in -val add_locale = gen_add_locale read_context; -val add_locale_i = gen_add_locale cert_context; +val add_locale = gen_add_locale read_declaration; +val add_locale_i = gen_add_locale cert_declaration; end; @@ -752,28 +796,17 @@ local -fun store_dep target ((name, morph), thms) = - NewLocale.add_dependency target (name, morph $> Element.satisfy_morphism thms); - fun gen_sublocale prep_expr after_qed target expression thy = let val target_ctxt = NewLocale.init target thy; val target' = NewLocale.intern thy target; - val ((_, fixed, deps, _, _), _) = prep_expr true true target_ctxt expression [] []; - val (_, goal_ctxt) = ProofContext.add_fixes_i fixed target_ctxt; + val ((propss, deps, export'), goal_ctxt) = prep_expr expression target_ctxt; + + fun store_dep target ((name, morph), thms) = + NewLocale.add_dependency target (name, morph $> Element.satisfy_morphism thms $> export'); - (* proof obligations from deps *) - fun props_of (name, morph) = - let - val (asm, defs) = NewLocale.specification_of thy name; - in - (case asm of NONE => defs | SOME asm => asm :: defs) |> map (Morphism.term morph) - end; - - val propss = map props_of deps; - fun after_qed' results = fold (store_dep target') (deps ~~ prep_result propss results) #> after_qed results; @@ -786,8 +819,8 @@ in -fun sublocale x = gen_sublocale read_full_context_statement x; -fun sublocale_i x = gen_sublocale cert_full_context_statement x; +fun sublocale x = gen_sublocale read_goal_expression x; +fun sublocale_i x = gen_sublocale cert_goal_expression x; end;