Interpretation in proof contexts.
authorballarin
Fri Dec 05 16:41:36 2008 +0100 (2008-12-05)
changeset 2901817538bdef546
parent 28994 49f602ae24e5
child 29019 8e7d6f959bd7
Interpretation in proof contexts.
src/FOL/ex/NewLocaleSetup.thy
src/FOL/ex/NewLocaleTest.thy
src/Pure/Isar/expression.ML
src/Pure/Isar/new_locale.ML
     1.1 --- a/src/FOL/ex/NewLocaleSetup.thy	Fri Dec 05 11:42:27 2008 +0100
     1.2 +++ b/src/FOL/ex/NewLocaleSetup.thy	Fri Dec 05 16:41:36 2008 +0100
     1.3 @@ -41,11 +41,19 @@
     1.4  
     1.5  val _ =
     1.6    OuterSyntax.command "interpretation"
     1.7 -    "prove and register interpretation of locale expression in theory" K.thy_goal
     1.8 +    "prove interpretation of locale expression in theory" K.thy_goal
     1.9      (P.!!! Expression.parse_expression
    1.10          >> (fn expr => Toplevel.print o
    1.11              Toplevel.theory_to_proof (Expression.interpretation_cmd expr)));
    1.12  
    1.13 +val _ =
    1.14 +  OuterSyntax.command "interpret"
    1.15 +    "prove interpretation of locale expression in proof context"
    1.16 +    (K.tag_proof K.prf_goal)
    1.17 +    (P.!!! Expression.parse_expression
    1.18 +        >> (fn expr => Toplevel.print o
    1.19 +            Toplevel.proof' (fn int => Expression.interpret_cmd expr int)));
    1.20 +
    1.21  end
    1.22  
    1.23  *}
     2.1 --- a/src/FOL/ex/NewLocaleTest.thy	Fri Dec 05 11:42:27 2008 +0100
     2.2 +++ b/src/FOL/ex/NewLocaleTest.thy	Fri Dec 05 16:41:36 2008 +0100
     2.3 @@ -341,4 +341,24 @@
     2.4  
     2.5  thm two.assoc
     2.6  
     2.7 +
     2.8 +text {* Interpretation in proofs *}
     2.9 +
    2.10 +lemma True
    2.11 +proof
    2.12 +  interpret "local": lgrp "op +" "0" "minus"
    2.13 +    by unfold_locales  (* subsumed *)
    2.14 +  {
    2.15 +    fix zero :: int
    2.16 +    assume "!!x. zero + x = x" "!!x. (-x) + x = zero"
    2.17 +    then interpret local_fixed: lgrp "op +" zero "minus"
    2.18 +      by unfold_locales
    2.19 +    thm local_fixed.lone
    2.20 +  }
    2.21 +  assume "!!x zero. zero + x = x" "!!x zero. (-x) + x = zero"
    2.22 +  then interpret local_free: lgrp "op +" zero "minus" for zero
    2.23 +    by unfold_locales
    2.24 +  thm local_free.lone [where ?zero = 0]
    2.25 +qed
    2.26 +
    2.27  end
     3.1 --- a/src/Pure/Isar/expression.ML	Fri Dec 05 11:42:27 2008 +0100
     3.2 +++ b/src/Pure/Isar/expression.ML	Fri Dec 05 16:41:36 2008 +0100
     3.3 @@ -28,10 +28,8 @@
     3.4    val sublocale: string -> expression_i -> theory -> Proof.state;
     3.5    val interpretation_cmd: expression -> theory -> Proof.state;
     3.6    val interpretation: expression_i -> theory -> Proof.state;
     3.7 -(*
     3.8 -  val interpret_cmd: Morphism.morphism -> expression -> bool -> Proof.state -> Proof.state;
     3.9 -  val interpret: Morphism.morphism -> expression_i -> bool -> Proof.state -> Proof.state;
    3.10 -*)
    3.11 +  val interpret_cmd: expression -> bool -> Proof.state -> Proof.state;
    3.12 +  val interpret: expression_i -> bool -> Proof.state -> Proof.state;
    3.13  
    3.14    (* Debugging and development *)
    3.15    val parse_expression: OuterParse.token list -> expression * OuterParse.token list
    3.16 @@ -538,14 +536,12 @@
    3.17  
    3.18  fun prep_declaration prep activate raw_import raw_elems context =
    3.19    let
    3.20 -    val thy = ProofContext.theory_of context;
    3.21 -
    3.22      val ((fixed, deps, elems, _), (parms, (spec, (_, _, defs)))) =
    3.23        prep false true context raw_import raw_elems [];
    3.24      (* Declare parameters and imported facts *)
    3.25      val context' = context |>
    3.26        ProofContext.add_fixes_i fixed |> snd |>
    3.27 -      NewLocale.clear_local_idents |> fold (NewLocale.activate_local_facts thy) deps;
    3.28 +      NewLocale.clear_local_idents |> fold NewLocale.activate_local_facts deps;
    3.29      val ((elems', _), _) = activate elems (ProofContext.set_stmt true context');
    3.30    in ((fixed, deps, elems'), (parms, spec, defs)) end;
    3.31  
    3.32 @@ -837,6 +833,7 @@
    3.33  
    3.34  end;
    3.35  
    3.36 +
    3.37  (** Interpretation in theories **)
    3.38  
    3.39  local
    3.40 @@ -846,7 +843,7 @@
    3.41    let
    3.42      val ctxt = ProofContext.init thy;
    3.43  
    3.44 -    val ((propss, deps, export), goal_ctxt) = prep_expr expression ctxt;
    3.45 +    val ((propss, regs, export), goal_ctxt) = prep_expr expression ctxt;
    3.46      
    3.47      fun store_reg ((name, morph), thms) =
    3.48        let
    3.49 @@ -857,7 +854,7 @@
    3.50        end;
    3.51  
    3.52      fun after_qed results =
    3.53 -      ProofContext.theory (fold store_reg (deps ~~ prep_result propss results));
    3.54 +      ProofContext.theory (fold store_reg (regs ~~ prep_result propss results));
    3.55    in
    3.56      goal_ctxt |>
    3.57        Proof.theorem_i NONE after_qed (prep_propp propss) |>
    3.58 @@ -871,5 +868,41 @@
    3.59  
    3.60  end;
    3.61  
    3.62 +
    3.63 +(** Interpretation in proof contexts **)
    3.64 +
    3.65 +local
    3.66 +
    3.67 +fun gen_interpret prep_expr
    3.68 +    expression int state =
    3.69 +  let
    3.70 +    val _ = Proof.assert_forward_or_chain state;
    3.71 +    val ctxt = Proof.context_of state;
    3.72 +
    3.73 +    val ((propss, regs, export), goal_ctxt) = prep_expr expression ctxt;
    3.74 +    
    3.75 +    fun store_reg ((name, morph), thms) =
    3.76 +      let
    3.77 +        val morph' = morph $> Element.satisfy_morphism thms $> export;
    3.78 +      in
    3.79 +        NewLocale.activate_local_facts (name, morph')
    3.80 +      end;
    3.81 +
    3.82 +    fun after_qed results =
    3.83 +      Proof.map_context (fold store_reg (regs ~~ prep_result propss results)) #> Seq.single;
    3.84 +  in
    3.85 +    state |> Proof.map_context (K goal_ctxt) |>
    3.86 +      Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
    3.87 +      "interpret" NONE after_qed (map (pair (Binding.empty, [])) (prep_propp propss)) |>
    3.88 +      Element.refine_witness |> Seq.hd
    3.89 +  end;
    3.90 +
    3.91 +in
    3.92 +
    3.93 +fun interpret_cmd x = gen_interpret read_goal_expression x;
    3.94 +fun interpret x = gen_interpret cert_goal_expression x;
    3.95 +
    3.96  end;
    3.97  
    3.98 +end;
    3.99 +
     4.1 --- a/src/Pure/Isar/new_locale.ML	Fri Dec 05 11:42:27 2008 +0100
     4.2 +++ b/src/Pure/Isar/new_locale.ML	Fri Dec 05 16:41:36 2008 +0100
     4.3 @@ -37,10 +37,8 @@
     4.4    (* Activation *)
     4.5    val activate_declarations: theory -> string * Morphism.morphism ->
     4.6      Proof.context -> Proof.context
     4.7 -  val activate_global_facts: string * Morphism.morphism ->
     4.8 -    theory -> theory
     4.9 -  val activate_local_facts: theory -> string * Morphism.morphism ->
    4.10 -    Proof.context -> Proof.context
    4.11 +  val activate_global_facts: string * Morphism.morphism -> theory -> theory
    4.12 +  val activate_local_facts: string * Morphism.morphism -> Proof.context -> Proof.context
    4.13  (*  val activate: string -> theory -> (Element.context_i -> 'a -> 'a) -> 'a -> 'a *)
    4.14    val init: string -> theory -> Proof.context
    4.15  
    4.16 @@ -360,8 +358,9 @@
    4.17    roundup thy (activate_notes init_global_elem) dep (get_global_idents thy, thy) |>
    4.18    uncurry put_global_idents;
    4.19  
    4.20 -fun activate_local_facts thy dep ctxt =
    4.21 -  roundup thy (activate_notes init_local_elem) dep (get_local_idents ctxt, ctxt) |>
    4.22 +fun activate_local_facts dep ctxt =
    4.23 +  roundup (ProofContext.theory_of ctxt) (activate_notes init_local_elem) dep
    4.24 +    (get_local_idents ctxt, ctxt) |>
    4.25    uncurry put_local_idents;
    4.26  
    4.27  fun init name thy = activate_all name thy init_local_elem (empty, ProofContext.init thy) |>
    4.28 @@ -454,8 +453,9 @@
    4.29        "back-chain all introduction rules of locales")]));
    4.30  
    4.31  
    4.32 -(*** Registrations: interpretations in theories and proof contexts ***)
    4.33 +(*** Registrations: interpretations in theories ***)
    4.34  
    4.35 +(* FIXME only global variant needed *)
    4.36  structure RegistrationsData = GenericDataFun
    4.37  (
    4.38    type T = ((string * Morphism.morphism) * stamp) list;
    4.39 @@ -470,6 +470,5 @@
    4.40  fun add_global_registration reg =
    4.41    (Context.theory_map o RegistrationsData.map) (cons (reg, stamp ()));
    4.42  
    4.43 -
    4.44  end;
    4.45