# HG changeset patch # User ballarin # Date 1280603660 -7200 # Node ID b4115423c049d756dda3609227eb4593ca4be7a4 # Parent 3a46cebd79838d0a902a5ca0ab095a10738cadce Interpretation in proofs supports mixins. diff -r 3a46cebd7983 -r b4115423c049 src/FOL/ex/Locale_Test/Locale_Test1.thy --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Sat Jul 31 21:14:20 2010 +0200 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Sat Jul 31 21:14:20 2010 +0200 @@ -714,4 +714,25 @@ thm local_free.lone [where ?zero = 0] qed +lemma True +proof + { + fix pand and pnot and por + assume passoc: "!!x y z. pand(pand(x, y), z) <-> pand(x, pand(y, z))" + and pnotnot: "!!x. pnot(pnot(x)) <-> x" + and por_def: "!!x y. por(x, y) <-> pnot(pand(pnot(x), pnot(y)))" + interpret loc: logic_o pand pnot + where por_eq: "!!x y. logic_o.lor_o(pand, pnot, x, y) <-> por(x, y)" (* FIXME *) + proof - + show logic_o: "PROP logic_o(pand, pnot)" using passoc pnotnot by unfold_locales + fix x y + show "logic_o.lor_o(pand, pnot, x, y) <-> por(x, y)" + by (unfold logic_o.lor_o_def [OF logic_o]) (rule por_def [symmetric]) + qed + print_interps logic_o (* FIXME *) + thm loc.lor_o_def por_eq + have "!!x y. por(x, y) <-> pnot(pand(pnot(x), pnot(y)))" by (rule loc.lor_o_def) + } +qed + end diff -r 3a46cebd7983 -r b4115423c049 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Sat Jul 31 21:14:20 2010 +0200 +++ b/src/Pure/Isar/element.ML Sat Jul 31 21:14:20 2010 +0200 @@ -40,6 +40,9 @@ term list list -> term list -> Proof.context -> Proof.state val witness_local_proof: (witness list list -> Proof.state -> Proof.state) -> string -> term list list -> Proof.context -> bool -> Proof.state -> Proof.state + val witness_local_proof_eqs: (witness list list -> thm list -> Proof.state -> Proof.state) -> + string -> term list list -> term list -> Proof.context -> bool -> Proof.state -> + Proof.state val morph_witness: morphism -> witness -> witness val conclude_witness: witness -> thm val pretty_witness: Proof.context -> witness -> Pretty.T @@ -57,6 +60,8 @@ (Attrib.binding * (thm list * Attrib.src list) list) list val eq_morphism: theory -> thm list -> morphism option val transfer_morphism: theory -> morphism + val generic_note_thmss: string -> (Attrib.binding * (thm list * Attrib.src list) list) list -> + Context.generic -> (string * thm list) list * Context.generic val init: context_i -> Context.generic -> Context.generic val activate_i: context_i -> Proof.context -> context_i * Proof.context val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context @@ -280,6 +285,10 @@ in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end; in proof after_qed' propss #> refine_witness #> Seq.hd end; +fun proof_local cmd goal_ctxt int after_qed' propss = + Proof.map_context (K goal_ctxt) + #> Proof.local_goal (Proof_Display.print_results int) (K I) ProofContext.bind_propp_i + cmd NONE after_qed' (map (pair Thm.empty_binding) propss); in fun witness_proof after_qed wit_propss = @@ -289,12 +298,11 @@ val witness_proof_eqs = gen_witness_proof (Proof.theorem NONE); fun witness_local_proof after_qed cmd wit_propss goal_ctxt int = - gen_witness_proof (fn after_qed' => fn propss => - Proof.map_context (K goal_ctxt) - #> Proof.local_goal (Proof_Display.print_results int) (K I) ProofContext.bind_propp_i - cmd NONE after_qed' (map (pair Thm.empty_binding) propss)) + gen_witness_proof (proof_local cmd goal_ctxt int) (fn wits => fn _ => after_qed wits) wit_propss []; +fun witness_local_proof_eqs after_qed cmd wit_propss eq_props goal_ctxt int = + gen_witness_proof (proof_local cmd goal_ctxt int) after_qed wit_propss eq_props; end; @@ -467,6 +475,15 @@ (* init *) +fun generic_note_thmss kind facts context = + let + val facts' = Attrib.map_facts (Attrib.attribute_i (Context.theory_of context)) facts; + in + context |> Context.mapping_result + (PureThy.note_thmss kind facts') + (ProofContext.note_thmss kind facts') + end; + fun init (Fixes fixes) = Context.map_proof (ProofContext.add_fixes fixes #> #2) | init (Constrains _) = I | init (Assumes asms) = Context.map_proof (fn ctxt => @@ -486,13 +503,7 @@ |> fold Variable.auto_fixes (map #1 asms) |> ProofContext.add_assms_i Local_Defs.def_export (map #2 asms); in ctxt' end) - | init (Notes (kind, facts)) = (fn context => - let - val facts' = Attrib.map_facts (Attrib.attribute_i (Context.theory_of context)) facts; - val context' = context |> Context.mapping - (PureThy.note_thmss kind facts' #> #2) - (ProofContext.note_thmss kind facts' #> #2); - in context' end); + | init (Notes (kind, facts)) = generic_note_thmss kind facts #> #2; (* activate *) diff -r 3a46cebd7983 -r b4115423c049 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Sat Jul 31 21:14:20 2010 +0200 +++ b/src/Pure/Isar/expression.ML Sat Jul 31 21:14:20 2010 +0200 @@ -43,8 +43,8 @@ val sublocale_cmd: string -> expression -> theory -> Proof.state val interpretation: expression_i -> (Attrib.binding * term) list -> theory -> Proof.state val interpretation_cmd: expression -> (Attrib.binding * string) list -> theory -> Proof.state - val interpret: expression_i -> bool -> Proof.state -> Proof.state - val interpret_cmd: expression -> bool -> Proof.state -> Proof.state + val interpret: expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state + val interpret_cmd: expression -> (Attrib.binding * string) list -> bool -> Proof.state -> Proof.state end; structure Expression : EXPRESSION = @@ -790,10 +790,29 @@ (*** Interpretation ***) -(** Interpretation in theories **) +(** Interpretation in theories and proof contexts **) local +fun note_eqns_register deps witss attrss eqns export export' context = + let + fun meta_rewrite context = + map (Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def) o + maps snd; + in + context + |> Element.generic_note_thmss Thm.lemmaK + (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn],[])]) eqns) + |-> (fn facts => `(fn context => meta_rewrite context facts)) + |-> (fn eqns => fold (fn ((dep, morph), wits) => + fn context => + Locale.add_registration (dep, morph $> Element.satisfy_morphism + (map (Element.morph_witness export') wits)) + (Element.eq_morphism (Context.theory_of context) eqns |> + Option.map (rpair true)) + export context) (deps ~~ witss)) + end; + fun gen_interpretation prep_expr parse_prop prep_attr expression equations theory = let @@ -805,36 +824,42 @@ val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt; val export' = Variable.export_morphism goal_ctxt expr_ctxt; - fun note_eqns raw_eqns thy = - let - val eqns = map (Morphism.thm (export' $> export)) raw_eqns; - val eqn_attrss = map2 (fn attrs => fn eqn => - ((apsnd o map) (Attrib.attribute_i thy) attrs, [([eqn], [])])) attrss eqns; - fun meta_rewrite thy = - map (Local_Defs.meta_rewrite_rule (ProofContext.init_global thy) #> Drule.abs_def) o - maps snd; - in - thy - |> PureThy.note_thmss Thm.lemmaK eqn_attrss - |-> (fn facts => `(fn thy => meta_rewrite thy facts)) - end; - - fun after_qed witss eqns = ProofContext.theory (note_eqns eqns - #-> (fn eqns => fold (fn ((dep, morph), wits) => - fn thy => Context.theory_map - (Locale.add_registration (dep, morph $> Element.satisfy_morphism - (map (Element.morph_witness export') wits)) - (Element.eq_morphism thy eqns |> Option.map (rpair true)) - export) thy) (deps ~~ witss))); + fun after_qed witss eqns = (ProofContext.theory o Context.theory_map) + (note_eqns_register deps witss attrss eqns export export'); in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end; +fun gen_interpret prep_expr parse_prop prep_attr + expression equations int state = + let + val _ = Proof.assert_forward_or_chain state; + val ctxt = Proof.context_of state; + val theory = ProofContext.theory_of ctxt; + + val ((propss, deps, export), expr_ctxt) = prep_expr expression ctxt; + + val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt; + val attrss = map ((apsnd o map) (prep_attr theory) o fst) equations; + val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt; + val export' = Variable.export_morphism goal_ctxt expr_ctxt; + + fun after_qed witss eqns = (Proof.map_context o Context.proof_map) + (note_eqns_register deps witss attrss eqns export export'); + in + state + |> Element.witness_local_proof_eqs after_qed "interpret" propss eqns goal_ctxt int + end; + in fun interpretation x = gen_interpretation cert_goal_expression (K I) (K I) x; fun interpretation_cmd x = gen_interpretation read_goal_expression Syntax.parse_prop Attrib.intern_src x; +fun interpret x = gen_interpret cert_goal_expression (K I) (K I) x; +fun interpret_cmd x = gen_interpret read_goal_expression + Syntax.parse_prop Attrib.intern_src x; + end; @@ -859,36 +884,5 @@ end; - -(** Interpretation in proof contexts **) - -local - -fun gen_interpret prep_expr expression int state = - let - val _ = Proof.assert_forward_or_chain state; - val ctxt = Proof.context_of state; - - val ((propss, regs, export), goal_ctxt) = prep_expr expression ctxt; - - fun store_reg (name, morph) thms = - let - val morph' = morph $> Element.satisfy_morphism thms $> export; - in Context.proof_map (Locale.activate_facts (name, morph')) end; - - fun after_qed wits = - Proof.map_context (fold2 store_reg regs wits); - in - state - |> Element.witness_local_proof after_qed "interpret" propss goal_ctxt int - end; - -in - -fun interpret x = gen_interpret cert_goal_expression x; -fun interpret_cmd x = gen_interpret read_goal_expression x; - end; -end; - diff -r 3a46cebd7983 -r b4115423c049 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Sat Jul 31 21:14:20 2010 +0200 +++ b/src/Pure/Isar/isar_syn.ML Sat Jul 31 21:14:20 2010 +0200 @@ -444,8 +444,10 @@ Outer_Syntax.command "interpret" "prove interpretation of locale expression in proof context" (Keyword.tag_proof Keyword.prf_goal) - (Parse.!!! (Parse_Spec.locale_expression true) - >> (fn expr => Toplevel.print o Toplevel.proof' (Expression.interpret_cmd expr))); + (Parse.!!! (Parse_Spec.locale_expression true) -- + Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [] + >> (fn (expr, equations) => Toplevel.print o + Toplevel.proof' (Expression.interpret_cmd expr equations))); (* classes *)