# HG changeset patch # User haftmann # Date 1392843905 -3600 # Node ID 6535c537b2436dd317acbd84d7f2d3005ea48986 # Parent da35747597bdfa1d578db5e9938532069577c124 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation" diff -r da35747597bd -r 6535c537b243 src/HOL/IMP/Abs_Int1_const.thy --- a/src/HOL/IMP/Abs_Int1_const.thy Thu Feb 20 12:27:51 2014 +1100 +++ b/src/HOL/IMP/Abs_Int1_const.thy Wed Feb 19 22:05:05 2014 +0100 @@ -53,7 +53,7 @@ end -interpretation Val_semilattice +permanent_interpretation Val_semilattice where \ = \_const and num' = Const and plus' = plus_const proof case goal1 thus ?case @@ -67,7 +67,7 @@ by(auto simp: plus_const_cases split: const.split) qed -interpretation Abs_Int +permanent_interpretation Abs_Int where \ = \_const and num' = Const and plus' = plus_const defines AI_const is AI and step_const is step' and aval'_const is aval' .. @@ -121,7 +121,7 @@ text{* Monotonicity: *} -interpretation Abs_Int_mono +permanent_interpretation Abs_Int_mono where \ = \_const and num' = Const and plus' = plus_const proof case goal1 thus ?case @@ -133,7 +133,7 @@ definition m_const :: "const \ nat" where "m_const x = (if x = Any then 0 else 1)" -interpretation Abs_Int_measure +permanent_interpretation Abs_Int_measure where \ = \_const and num' = Const and plus' = plus_const and m = m_const and h = "1" proof diff -r da35747597bd -r 6535c537b243 src/HOL/IMP/Abs_Int1_parity.thy --- a/src/HOL/IMP/Abs_Int1_parity.thy Thu Feb 20 12:27:51 2014 +1100 +++ b/src/HOL/IMP/Abs_Int1_parity.thy Wed Feb 19 22:05:05 2014 +0100 @@ -102,7 +102,7 @@ text{* First we instantiate the abstract value interface and prove that the functions on type @{typ parity} have all the necessary properties: *} -interpretation Val_semilattice +permanent_interpretation Val_semilattice where \ = \_parity and num' = num_parity and plus' = plus_parity proof txt{* of the locale axioms *} fix a b :: parity @@ -123,7 +123,7 @@ proofs (they happened in the instatiation above) but delivers the instantiated abstract interpreter which we call @{text AI_parity}: *} -interpretation Abs_Int +permanent_interpretation Abs_Int where \ = \_parity and num' = num_parity and plus' = plus_parity defines aval_parity is aval' and step_parity is step' and AI_parity is AI .. @@ -154,7 +154,7 @@ subsubsection "Termination" -interpretation Abs_Int_mono +permanent_interpretation Abs_Int_mono where \ = \_parity and num' = num_parity and plus' = plus_parity proof case goal1 thus ?case @@ -165,7 +165,7 @@ definition m_parity :: "parity \ nat" where "m_parity x = (if x = Either then 0 else 1)" -interpretation Abs_Int_measure +permanent_interpretation Abs_Int_measure where \ = \_parity and num' = num_parity and plus' = plus_parity and m = m_parity and h = "1" proof diff -r da35747597bd -r 6535c537b243 src/HOL/IMP/Abs_Int2_ivl.thy --- a/src/HOL/IMP/Abs_Int2_ivl.thy Thu Feb 20 12:27:51 2014 +1100 +++ b/src/HOL/IMP/Abs_Int2_ivl.thy Wed Feb 19 22:05:05 2014 +0100 @@ -302,7 +302,7 @@ "\Fin y1 \ x1; Fin y2 \ x2\ \ Fin(y1 + y2::'a::ordered_ab_group_add) \ x1 + x2" by(drule (1) add_mono) simp -interpretation Val_semilattice +permanent_interpretation Val_semilattice where \ = \_ivl and num' = num_ivl and plus' = "op +" proof case goal1 thus ?case by transfer (simp add: le_iff_subset) @@ -318,7 +318,7 @@ qed -interpretation Val_lattice_gamma +permanent_interpretation Val_lattice_gamma where \ = \_ivl and num' = num_ivl and plus' = "op +" defines aval_ivl is aval' proof @@ -327,7 +327,7 @@ case goal2 show ?case unfolding bot_ivl_def by transfer simp qed -interpretation Val_inv +permanent_interpretation Val_inv where \ = \_ivl and num' = num_ivl and plus' = "op +" and test_num' = in_ivl and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl @@ -350,7 +350,7 @@ done qed -interpretation Abs_Int_inv +permanent_interpretation Abs_Int_inv where \ = \_ivl and num' = num_ivl and plus' = "op +" and test_num' = in_ivl and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl @@ -384,7 +384,7 @@ apply(auto simp: below_rep_def le_iff_subset split: if_splits prod.split) by(auto simp: is_empty_rep_iff \_rep_cases split: extended.splits) -interpretation Abs_Int_inv_mono +permanent_interpretation Abs_Int_inv_mono where \ = \_ivl and num' = num_ivl and plus' = "op +" and test_num' = in_ivl and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl diff -r da35747597bd -r 6535c537b243 src/HOL/IMP/Abs_Int3.thy --- a/src/HOL/IMP/Abs_Int3.thy Thu Feb 20 12:27:51 2014 +1100 +++ b/src/HOL/IMP/Abs_Int3.thy Wed Feb 19 22:05:05 2014 +0100 @@ -260,7 +260,7 @@ end -interpretation Abs_Int_wn +permanent_interpretation Abs_Int_wn where \ = \_ivl and num' = num_ivl and plus' = "op +" and test_num' = in_ivl and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl @@ -545,7 +545,7 @@ split: prod.splits if_splits extended.split) -interpretation Abs_Int_wn_measure +permanent_interpretation Abs_Int_wn_measure where \ = \_ivl and num' = num_ivl and plus' = "op +" and test_num' = in_ivl and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl diff -r da35747597bd -r 6535c537b243 src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Thu Feb 20 12:27:51 2014 +1100 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Wed Feb 19 22:05:05 2014 +0100 @@ -47,13 +47,13 @@ end -interpretation Rep rep_cval +permanent_interpretation Rep rep_cval proof case goal1 thus ?case by(cases a, cases b, simp, simp, cases b, simp, simp) qed -interpretation Val_abs rep_cval Const plus_cval +permanent_interpretation Val_abs rep_cval Const plus_cval proof case goal1 show ?case by simp next @@ -61,7 +61,7 @@ by(cases a1, cases a2, simp, simp, cases a2, simp, simp) qed -interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)" +permanent_interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)" defines AI_const is AI and aval'_const is aval' proof qed (auto simp: iter'_pfp_above) diff -r da35747597bd -r 6535c537b243 src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Thu Feb 20 12:27:51 2014 +1100 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Wed Feb 19 22:05:05 2014 +0100 @@ -166,13 +166,13 @@ I (max_option False (l1 + Some 1) l2) h2) else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))" -interpretation Rep rep_ivl +permanent_interpretation Rep rep_ivl proof case goal1 thus ?case by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits) qed -interpretation Val_abs rep_ivl num_ivl plus_ivl +permanent_interpretation Val_abs rep_ivl num_ivl plus_ivl proof case goal1 thus ?case by(simp add: rep_ivl_def num_ivl_def) next @@ -180,7 +180,7 @@ by(auto simp add: rep_ivl_def plus_ivl_def split: ivl.split option.splits) qed -interpretation Rep1 rep_ivl +permanent_interpretation Rep1 rep_ivl proof case goal1 thus ?case by(auto simp add: rep_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split) @@ -188,7 +188,7 @@ case goal2 show ?case by(auto simp add: Bot_ivl_def rep_ivl_def empty_def) qed -interpretation +permanent_interpretation Val_abs1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl proof case goal1 thus ?case @@ -200,7 +200,7 @@ auto simp: rep_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits) qed -interpretation +permanent_interpretation Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3)" defines afilter_ivl is afilter and bfilter_ivl is bfilter diff -r da35747597bd -r 6535c537b243 src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Thu Feb 20 12:27:51 2014 +1100 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Wed Feb 19 22:05:05 2014 +0100 @@ -192,7 +192,7 @@ end -interpretation +permanent_interpretation Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3 2)" defines afilter_ivl' is afilter and bfilter_ivl' is bfilter diff -r da35747597bd -r 6535c537b243 src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy Thu Feb 20 12:27:51 2014 +1100 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy Wed Feb 19 22:05:05 2014 +0100 @@ -52,7 +52,7 @@ end -interpretation Val_abs +permanent_interpretation Val_abs where \ = \_const and num' = Const and plus' = plus_const proof case goal1 thus ?case @@ -66,7 +66,7 @@ by(auto simp: plus_const_cases split: const.split) qed -interpretation Abs_Int +permanent_interpretation Abs_Int where \ = \_const and num' = Const and plus' = plus_const defines AI_const is AI and step_const is step' and aval'_const is aval' .. @@ -114,7 +114,7 @@ text{* Monotonicity: *} -interpretation Abs_Int_mono +permanent_interpretation Abs_Int_mono where \ = \_const and num' = Const and plus' = plus_const proof case goal1 thus ?case diff -r da35747597bd -r 6535c537b243 src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy Thu Feb 20 12:27:51 2014 +1100 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy Wed Feb 19 22:05:05 2014 +0100 @@ -113,7 +113,7 @@ proofs (they happened in the instatiation above) but delivers the instantiated abstract interpreter which we call AI: *} -interpretation Abs_Int +permanent_interpretation Abs_Int where \ = \_parity and num' = num_parity and plus' = plus_parity defines aval_parity is aval' and step_parity is step' and AI_parity is AI .. @@ -141,7 +141,7 @@ subsubsection "Termination" -interpretation Abs_Int_mono +permanent_interpretation Abs_Int_mono where \ = \_parity and num' = num_parity and plus' = plus_parity proof case goal1 thus ?case diff -r da35747597bd -r 6535c537b243 src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Thu Feb 20 12:27:51 2014 +1100 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Wed Feb 19 22:05:05 2014 +0100 @@ -165,7 +165,7 @@ I (max_option False (l1 + Some 1) l2) h2) else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))" -interpretation Val_abs +permanent_interpretation Val_abs where \ = \_ivl and num' = num_ivl and plus' = plus_ivl proof case goal1 thus ?case @@ -179,7 +179,7 @@ by(auto simp add: \_ivl_def plus_ivl_def split: ivl.split option.splits) qed -interpretation Val_abs1_gamma +permanent_interpretation Val_abs1_gamma where \ = \_ivl and num' = num_ivl and plus' = plus_ivl defines aval_ivl is aval' proof @@ -198,7 +198,7 @@ done -interpretation Val_abs1 +permanent_interpretation Val_abs1 where \ = \_ivl and num' = num_ivl and plus' = plus_ivl and test_num' = in_ivl and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl @@ -215,7 +215,7 @@ auto simp: \_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits) qed -interpretation Abs_Int1 +permanent_interpretation Abs_Int1 where \ = \_ivl and num' = num_ivl and plus' = plus_ivl and test_num' = in_ivl and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl @@ -229,7 +229,7 @@ text{* Monotonicity: *} -interpretation Abs_Int1_mono +permanent_interpretation Abs_Int1_mono where \ = \_ivl and num' = num_ivl and plus' = plus_ivl and test_num' = in_ivl and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl diff -r da35747597bd -r 6535c537b243 src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy Thu Feb 20 12:27:51 2014 +1100 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy Wed Feb 19 22:05:05 2014 +0100 @@ -225,7 +225,7 @@ end -interpretation Abs_Int2 +permanent_interpretation Abs_Int2 where \ = \_ivl and num' = num_ivl and plus' = plus_ivl and test_num' = in_ivl and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl diff -r da35747597bd -r 6535c537b243 src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy Thu Feb 20 12:27:51 2014 +1100 +++ b/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy Wed Feb 19 22:05:05 2014 +0100 @@ -89,7 +89,7 @@ WHILE b DO lift F c (sub\<^sub>1 ` M) {F (post ` M)}" -interpretation Complete_Lattice_ix "%c. {c'. strip c' = c}" "lift Inter" +permanent_interpretation Complete_Lattice_ix "%c. {c'. strip c' = c}" "lift Inter" proof case goal1 have "a:A \ lift Inter (strip a) A \ a" diff -r da35747597bd -r 6535c537b243 src/HOL/IMP/Collecting.thy --- a/src/HOL/IMP/Collecting.thy Thu Feb 20 12:27:51 2014 +1100 +++ b/src/HOL/IMP/Collecting.thy Wed Feb 19 22:05:05 2014 +0100 @@ -95,7 +95,7 @@ definition Inf_acom :: "com \ 'a::complete_lattice acom set \ 'a acom" where "Inf_acom c M = annotate (\p. INF C:M. anno C p) c" -interpretation +permanent_interpretation Complete_Lattice "{C. strip C = c}" "Inf_acom c" for c proof case goal1 thus ?case diff -r da35747597bd -r 6535c537b243 src/HOL/ex/Interpretation_with_Defs.thy --- a/src/HOL/ex/Interpretation_with_Defs.thy Thu Feb 20 12:27:51 2014 +1100 +++ b/src/HOL/ex/Interpretation_with_Defs.thy Wed Feb 19 22:05:05 2014 +0100 @@ -6,6 +6,7 @@ theory Interpretation_with_Defs imports Pure +keywords "permanent_interpretation" :: thy_goal begin ML_file "~~/src/Tools/interpretation_with_defs.ML" diff -r da35747597bd -r 6535c537b243 src/Tools/interpretation_with_defs.ML --- a/src/Tools/interpretation_with_defs.ML Thu Feb 20 12:27:51 2014 +1100 +++ b/src/Tools/interpretation_with_defs.ML Wed Feb 19 22:05:05 2014 +0100 @@ -6,87 +6,105 @@ signature INTERPRETATION_WITH_DEFS = sig - val interpretation: Expression.expression_i -> + val permanent_interpretation: Expression.expression_i -> (Attrib.binding * ((binding * mixfix) * term)) list -> (Attrib.binding * term) list -> - theory -> Proof.state - val interpretation_cmd: Expression.expression -> + local_theory -> Proof.state + val permanent_interpretation_cmd: Expression.expression -> (Attrib.binding * ((binding * mixfix) * string)) list -> (Attrib.binding * string) list -> - theory -> Proof.state + local_theory -> Proof.state end; structure Interpretation_With_Defs : INTERPRETATION_WITH_DEFS = struct -fun note_eqns_register deps witss def_eqns attrss eqns export export' = - let - fun meta_rewrite context = - map (Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def) o - maps snd; - in - Attrib.generic_notes 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.transform_witness export') wits)) - (Element.eq_morphism (Context.theory_of context) (def_eqns @ eqns) |> - Option.map (rpair true)) - export context) (deps ~~ witss)) - end; - local -fun gen_interpretation prep_expr prep_decl parse_term parse_prop prep_attr - expression raw_defs raw_eqns theory = +(* reading *) + +fun prep_interpretation prep_expr prep_term prep_prop prep_attr expression raw_defs raw_eqns initial_ctxt = let - val (_, (_, defs_ctxt)) = - prep_decl expression I [] (Proof_Context.init_global theory); - - val rhss = map (parse_term defs_ctxt o snd o snd) raw_defs - |> Syntax.check_terms defs_ctxt; - val defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs => - ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss; + (*reading*) + val ((_, deps, _), proto_deps_ctxt) = prep_expr expression initial_ctxt; + val deps_ctxt = fold Locale.activate_declarations deps proto_deps_ctxt; + val prep = Syntax.check_terms deps_ctxt #> Variable.export_terms deps_ctxt deps_ctxt; + val rhss = (prep o map (prep_term deps_ctxt o snd o snd)) raw_defs; + val eqns = (prep o map (prep_prop deps_ctxt o snd)) raw_eqns; - val (def_eqns, theory') = theory - |> Named_Target.theory_init - |> fold_map (Local_Theory.define) defs - |>> map (Thm.symmetric o snd o snd) - |> Local_Theory.exit_result_global (map o Morphism.thm); + (*defining*) + val pre_defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs => + ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss; + val (defs, defs_ctxt) = fold_map Local_Theory.define pre_defs initial_ctxt; + val def_eqns = map (Thm.symmetric o Morphism.thm (Local_Theory.standard_morphism defs_ctxt initial_ctxt) o snd o snd) defs; + val base_ctxt = if null def_eqns then defs_ctxt else Local_Theory.restore defs_ctxt; + (*the "if" prevents restoring a proof context which is no local theory*) - val ((propss, deps, export), expr_ctxt) = theory' - |> Proof_Context.init_global - |> prep_expr expression; - - val eqns = map (parse_prop expr_ctxt o snd) raw_eqns - |> Syntax.check_terms expr_ctxt; - val attrss = map ((apsnd o map) (prep_attr theory) o fst) raw_eqns; + (*setting up*) + val ((propss, deps, export), expr_ctxt) = prep_expr expression base_ctxt; + (*FIXME: only re-prepare if defs are given*) + val attrss = map (apsnd (map (prep_attr (Proof_Context.theory_of expr_ctxt))) o fst) raw_eqns; val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt; val export' = Variable.export_morphism goal_ctxt expr_ctxt; + in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end; +val cert_interpretation = prep_interpretation Expression.cert_goal_expression (K I) (K I) (K I); +val read_interpretation = prep_interpretation Expression.read_goal_expression Syntax.parse_term Syntax.parse_prop Attrib.intern_src; + + +(* generic interpretation machinery *) + +fun meta_rewrite eqns ctxt = (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt); + +fun note_eqns_register note activate deps witss def_eqns eqns attrss export export' ctxt = + let + val facts = (Attrib.empty_binding, [(map (Morphism.thm (export' $> export)) def_eqns, [])]) + :: map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns; + val (eqns', ctxt') = ctxt + |> note Thm.lemmaK facts + |-> meta_rewrite; + val dep_morphs = map2 (fn (dep, morph) => fn wits => + (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss; + fun activate' dep_morph ctxt = activate dep_morph + (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt; + in + ctxt' + |> fold activate' dep_morphs + end; + +fun generic_interpretation prep_interpretation setup_proof note add_registration + expression raw_defs raw_eqns initial_ctxt = + let + val (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) = + prep_interpretation expression raw_defs raw_eqns initial_ctxt; fun after_qed witss eqns = - (Proof_Context.background_theory o Context.theory_map) - (note_eqns_register deps witss def_eqns attrss eqns export export'); + note_eqns_register note add_registration deps witss def_eqns eqns attrss export export'; + in setup_proof after_qed propss eqns goal_ctxt end; + + +(* interpretation with permanent registration *) - in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end; +fun subscribe lthy = + if Named_Target.is_theory lthy + then Generic_Target.theory_registration + else Generic_Target.locale_dependency (Named_Target.the_name lthy); + +fun gen_permanent_interpretation prep_interpretation expression raw_defs raw_eqns lthy = + generic_interpretation prep_interpretation Element.witness_proof_eqs Local_Theory.notes_kind (subscribe lthy) + expression raw_defs raw_eqns lthy in -fun interpretation x = gen_interpretation Expression.cert_goal_expression - Expression.cert_declaration (K I) (K I) (K I) x; -fun interpretation_cmd x = gen_interpretation Expression.read_goal_expression - Expression.read_declaration Syntax.parse_term Syntax.parse_prop Attrib.intern_src x; +fun permanent_interpretation x = gen_permanent_interpretation cert_interpretation x; +fun permanent_interpretation_cmd x = gen_permanent_interpretation read_interpretation x; end; val _ = - Outer_Syntax.command @{command_spec "interpretation"} - "prove interpretation of locale expression in theory" + Outer_Syntax.local_theory_to_proof @{command_spec "permanent_interpretation"} + "prove interpretation of locale expression into named theory" (Parse.!!! (Parse_Spec.locale_expression true) -- Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "is"} -- Parse.term))) [] -- Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [] - >> (fn ((expr, defs), equations) => Toplevel.print o - Toplevel.theory_to_proof (interpretation_cmd expr defs equations))); + >> (fn ((expr, defs), eqns) => permanent_interpretation_cmd expr defs eqns)); end;