author ballarin Sat Jul 31 21:14:20 2010 +0200 (2010-07-31 ago) changeset 38108 b4115423c049 parent 38107 3a46cebd7983 child 38109 06fd1914b902
Interpretation in proofs supports mixins.
 src/FOL/ex/Locale_Test/Locale_Test1.thy file | annotate | diff | revisions src/Pure/Isar/element.ML file | annotate | diff | revisions src/Pure/Isar/expression.ML file | annotate | diff | revisions src/Pure/Isar/isar_syn.ML file | annotate | diff | revisions
```     1.1 --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Sat Jul 31 21:14:20 2010 +0200
1.2 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Sat Jul 31 21:14:20 2010 +0200
1.3 @@ -714,4 +714,25 @@
1.4    thm local_free.lone [where ?zero = 0]
1.5  qed
1.6
1.7 +lemma True
1.8 +proof
1.9 +  {
1.10 +    fix pand and pnot and por
1.11 +    assume passoc: "!!x y z. pand(pand(x, y), z) <-> pand(x, pand(y, z))"
1.12 +      and pnotnot: "!!x. pnot(pnot(x)) <-> x"
1.13 +      and por_def: "!!x y. por(x, y) <-> pnot(pand(pnot(x), pnot(y)))"
1.14 +    interpret loc: logic_o pand pnot
1.15 +      where por_eq: "!!x y. logic_o.lor_o(pand, pnot, x, y) <-> por(x, y)"  (* FIXME *)
1.16 +    proof -
1.17 +      show logic_o: "PROP logic_o(pand, pnot)" using passoc pnotnot by unfold_locales
1.18 +      fix x y
1.19 +      show "logic_o.lor_o(pand, pnot, x, y) <-> por(x, y)"
1.20 +        by (unfold logic_o.lor_o_def [OF logic_o]) (rule por_def [symmetric])
1.21 +    qed
1.22 +    print_interps logic_o  (* FIXME *)
1.23 +    thm loc.lor_o_def por_eq
1.24 +    have "!!x y. por(x, y) <-> pnot(pand(pnot(x), pnot(y)))" by (rule loc.lor_o_def)
1.25 +  }
1.26 +qed
1.27 +
1.28  end
```
```     2.1 --- a/src/Pure/Isar/element.ML	Sat Jul 31 21:14:20 2010 +0200
2.2 +++ b/src/Pure/Isar/element.ML	Sat Jul 31 21:14:20 2010 +0200
2.3 @@ -40,6 +40,9 @@
2.4      term list list -> term list -> Proof.context -> Proof.state
2.5    val witness_local_proof: (witness list list -> Proof.state -> Proof.state) ->
2.6      string -> term list list -> Proof.context -> bool -> Proof.state -> Proof.state
2.7 +  val witness_local_proof_eqs: (witness list list -> thm list -> Proof.state -> Proof.state) ->
2.8 +    string -> term list list -> term list -> Proof.context -> bool -> Proof.state ->
2.9 +    Proof.state
2.10    val morph_witness: morphism -> witness -> witness
2.11    val conclude_witness: witness -> thm
2.12    val pretty_witness: Proof.context -> witness -> Pretty.T
2.13 @@ -57,6 +60,8 @@
2.14      (Attrib.binding * (thm list * Attrib.src list) list) list
2.15    val eq_morphism: theory -> thm list -> morphism option
2.16    val transfer_morphism: theory -> morphism
2.17 +  val generic_note_thmss: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
2.18 +    Context.generic -> (string * thm list) list * Context.generic
2.19    val init: context_i -> Context.generic -> Context.generic
2.20    val activate_i: context_i -> Proof.context -> context_i * Proof.context
2.21    val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context
2.22 @@ -280,6 +285,10 @@
2.23        in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
2.24    in proof after_qed' propss #> refine_witness #> Seq.hd end;
2.25
2.26 +fun proof_local cmd goal_ctxt int after_qed' propss =
2.27 +    Proof.map_context (K goal_ctxt)
2.28 +    #> Proof.local_goal (Proof_Display.print_results int) (K I) ProofContext.bind_propp_i
2.29 +      cmd NONE after_qed' (map (pair Thm.empty_binding) propss);
2.30  in
2.31
2.32  fun witness_proof after_qed wit_propss =
2.33 @@ -289,12 +298,11 @@
2.34  val witness_proof_eqs = gen_witness_proof (Proof.theorem NONE);
2.35
2.36  fun witness_local_proof after_qed cmd wit_propss goal_ctxt int =
2.37 -  gen_witness_proof (fn after_qed' => fn propss =>
2.38 -    Proof.map_context (K goal_ctxt)
2.39 -    #> Proof.local_goal (Proof_Display.print_results int) (K I) ProofContext.bind_propp_i
2.40 -      cmd NONE after_qed' (map (pair Thm.empty_binding) propss))
2.41 +  gen_witness_proof (proof_local cmd goal_ctxt int)
2.42      (fn wits => fn _ => after_qed wits) wit_propss [];
2.43
2.44 +fun witness_local_proof_eqs after_qed cmd wit_propss eq_props goal_ctxt int =
2.45 +  gen_witness_proof (proof_local cmd goal_ctxt int) after_qed wit_propss eq_props;
2.46  end;
2.47
2.48
2.49 @@ -467,6 +475,15 @@
2.50
2.51  (* init *)
2.52
2.53 +fun generic_note_thmss kind facts context =
2.54 +  let
2.55 +    val facts' = Attrib.map_facts (Attrib.attribute_i (Context.theory_of context)) facts;
2.56 +  in
2.57 +    context |> Context.mapping_result
2.58 +      (PureThy.note_thmss kind facts')
2.59 +      (ProofContext.note_thmss kind facts')
2.60 +  end;
2.61 +
2.62  fun init (Fixes fixes) = Context.map_proof (ProofContext.add_fixes fixes #> #2)
2.63    | init (Constrains _) = I
2.64    | init (Assumes asms) = Context.map_proof (fn ctxt =>
2.65 @@ -486,13 +503,7 @@
2.66            |> fold Variable.auto_fixes (map #1 asms)
2.67            |> ProofContext.add_assms_i Local_Defs.def_export (map #2 asms);
2.68        in ctxt' end)
2.69 -  | init (Notes (kind, facts)) = (fn context =>
2.70 -      let
2.71 -        val facts' = Attrib.map_facts (Attrib.attribute_i (Context.theory_of context)) facts;
2.72 -        val context' = context |> Context.mapping
2.73 -          (PureThy.note_thmss kind facts' #> #2)
2.74 -          (ProofContext.note_thmss kind facts' #> #2);
2.75 -      in context' end);
2.76 +  | init (Notes (kind, facts)) = generic_note_thmss kind facts #> #2;
2.77
2.78
2.79  (* activate *)
```
```     3.1 --- a/src/Pure/Isar/expression.ML	Sat Jul 31 21:14:20 2010 +0200
3.2 +++ b/src/Pure/Isar/expression.ML	Sat Jul 31 21:14:20 2010 +0200
3.3 @@ -43,8 +43,8 @@
3.4    val sublocale_cmd: string -> expression -> theory -> Proof.state
3.5    val interpretation: expression_i -> (Attrib.binding * term) list -> theory -> Proof.state
3.6    val interpretation_cmd: expression -> (Attrib.binding * string) list -> theory -> Proof.state
3.7 -  val interpret: expression_i -> bool -> Proof.state -> Proof.state
3.8 -  val interpret_cmd: expression -> bool -> Proof.state -> Proof.state
3.9 +  val interpret: expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state
3.10 +  val interpret_cmd: expression -> (Attrib.binding * string) list -> bool -> Proof.state -> Proof.state
3.11  end;
3.12
3.13  structure Expression : EXPRESSION =
3.14 @@ -790,10 +790,29 @@
3.15
3.16  (*** Interpretation ***)
3.17
3.18 -(** Interpretation in theories **)
3.19 +(** Interpretation in theories and proof contexts **)
3.20
3.21  local
3.22
3.23 +fun note_eqns_register deps witss attrss eqns export export' context =
3.24 +  let
3.25 +    fun meta_rewrite context =
3.26 +      map (Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def) o
3.27 +        maps snd;
3.28 +  in
3.29 +    context
3.30 +    |> Element.generic_note_thmss Thm.lemmaK
3.31 +      (attrss ~~ map (fn eqn => [([Morphism.thm (export' \$> export) eqn],[])]) eqns)
3.32 +    |-> (fn facts => `(fn context => meta_rewrite context facts))
3.33 +    |-> (fn eqns => fold (fn ((dep, morph), wits) =>
3.34 +      fn context =>
3.35 +        Locale.add_registration (dep, morph \$> Element.satisfy_morphism
3.36 +            (map (Element.morph_witness export') wits))
3.37 +          (Element.eq_morphism (Context.theory_of context) eqns |>
3.38 +            Option.map (rpair true))
3.39 +          export context) (deps ~~ witss))
3.40 +  end;
3.41 +
3.42  fun gen_interpretation prep_expr parse_prop prep_attr
3.43      expression equations theory =
3.44    let
3.45 @@ -805,36 +824,42 @@
3.46      val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
3.47      val export' = Variable.export_morphism goal_ctxt expr_ctxt;
3.48
3.49 -    fun note_eqns raw_eqns thy =
3.50 -      let
3.51 -        val eqns = map (Morphism.thm (export' \$> export)) raw_eqns;
3.52 -        val eqn_attrss = map2 (fn attrs => fn eqn =>
3.53 -          ((apsnd o map) (Attrib.attribute_i thy) attrs, [([eqn], [])])) attrss eqns;
3.54 -        fun meta_rewrite thy =
3.55 -          map (Local_Defs.meta_rewrite_rule (ProofContext.init_global thy) #> Drule.abs_def) o
3.56 -            maps snd;
3.57 -      in
3.58 -        thy
3.59 -        |> PureThy.note_thmss Thm.lemmaK eqn_attrss
3.60 -        |-> (fn facts => `(fn thy => meta_rewrite thy facts))
3.61 -      end;
3.62 -
3.63 -    fun after_qed witss eqns = ProofContext.theory (note_eqns eqns
3.64 -      #-> (fn eqns => fold (fn ((dep, morph), wits) =>
3.65 -        fn thy => Context.theory_map
3.66 -          (Locale.add_registration (dep, morph \$> Element.satisfy_morphism
3.67 -              (map (Element.morph_witness export') wits))
3.68 -            (Element.eq_morphism thy eqns |> Option.map (rpair true))
3.69 -            export) thy) (deps ~~ witss)));
3.70 +    fun after_qed witss eqns = (ProofContext.theory o Context.theory_map)
3.71 +      (note_eqns_register deps witss attrss eqns export export');
3.72
3.73    in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
3.74
3.75 +fun gen_interpret prep_expr parse_prop prep_attr
3.76 +    expression equations int state =
3.77 +  let
3.78 +    val _ = Proof.assert_forward_or_chain state;
3.79 +    val ctxt = Proof.context_of state;
3.80 +    val theory = ProofContext.theory_of ctxt;
3.81 +
3.82 +    val ((propss, deps, export), expr_ctxt) = prep_expr expression ctxt;
3.83 +
3.84 +    val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
3.85 +    val attrss = map ((apsnd o map) (prep_attr theory) o fst) equations;
3.86 +    val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
3.87 +    val export' = Variable.export_morphism goal_ctxt expr_ctxt;
3.88 +
3.89 +    fun after_qed witss eqns = (Proof.map_context o Context.proof_map)
3.90 +      (note_eqns_register deps witss attrss eqns export export');
3.91 +  in
3.92 +    state
3.93 +    |> Element.witness_local_proof_eqs after_qed "interpret" propss eqns goal_ctxt int
3.94 +  end;
3.95 +
3.96  in
3.97
3.98  fun interpretation x = gen_interpretation cert_goal_expression (K I) (K I) x;
3.99  fun interpretation_cmd x = gen_interpretation read_goal_expression
3.100    Syntax.parse_prop Attrib.intern_src x;
3.101
3.102 +fun interpret x = gen_interpret cert_goal_expression (K I) (K I) x;
3.103 +fun interpret_cmd x = gen_interpret read_goal_expression
3.104 +  Syntax.parse_prop Attrib.intern_src x;
3.105 +
3.106  end;
3.107
3.108
3.109 @@ -859,36 +884,5 @@
3.110
3.111  end;
3.112
3.113 -
3.114 -(** Interpretation in proof contexts **)
3.115 -
3.116 -local
3.117 -
3.118 -fun gen_interpret prep_expr expression int state =
3.119 -  let
3.120 -    val _ = Proof.assert_forward_or_chain state;
3.121 -    val ctxt = Proof.context_of state;
3.122 -
3.123 -    val ((propss, regs, export), goal_ctxt) = prep_expr expression ctxt;
3.124 -
3.125 -    fun store_reg (name, morph) thms =
3.126 -      let
3.127 -        val morph' = morph \$> Element.satisfy_morphism thms \$> export;
3.128 -      in Context.proof_map (Locale.activate_facts (name, morph')) end;
3.129 -
3.130 -    fun after_qed wits =
3.131 -      Proof.map_context (fold2 store_reg regs wits);
3.132 -  in
3.133 -    state
3.134 -    |> Element.witness_local_proof after_qed "interpret" propss goal_ctxt int
3.135 -  end;
3.136 -
3.137 -in
3.138 -
3.139 -fun interpret x = gen_interpret cert_goal_expression x;
3.140 -fun interpret_cmd x = gen_interpret read_goal_expression x;
3.141 -
3.142  end;
3.143
3.144 -end;
3.145 -
```
```     4.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Jul 31 21:14:20 2010 +0200
4.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Jul 31 21:14:20 2010 +0200
4.3 @@ -444,8 +444,10 @@
4.4    Outer_Syntax.command "interpret"
4.5      "prove interpretation of locale expression in proof context"
4.6      (Keyword.tag_proof Keyword.prf_goal)
4.7 -    (Parse.!!! (Parse_Spec.locale_expression true)
4.8 -      >> (fn expr => Toplevel.print o Toplevel.proof' (Expression.interpret_cmd expr)));
4.9 +    (Parse.!!! (Parse_Spec.locale_expression true) --
4.10 +      Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
4.11 +      >> (fn (expr, equations) => Toplevel.print o
4.12 +          Toplevel.proof' (Expression.interpret_cmd expr equations)));
4.13
4.14
4.15  (* classes *)
```