Interpretation in proofs supports mixins.
authorballarin
Sat Jul 31 21:14:20 2010 +0200 (2010-07-31)
changeset 38108b4115423c049
parent 38107 3a46cebd7983
child 38109 06fd1914b902
Interpretation in proofs supports mixins.
src/FOL/ex/Locale_Test/Locale_Test1.thy
src/Pure/Isar/element.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/isar_syn.ML
     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 *)