diff --git a/Isabelle_DOF-Proofs/Reification_Test.thy b/Isabelle_DOF-Proofs/Reification_Test.thy index 780011c2..35c5b776 100644 --- a/Isabelle_DOF-Proofs/Reification_Test.thy +++ b/Isabelle_DOF-Proofs/Reification_Test.thy @@ -178,12 +178,12 @@ ML\ val A = Free ("A", propT); val B = Free ("B", propT); val t = Logic.mk_equals (A, B) -val tt = ISA_core.reify_term t +val tt = Meta_ISA_core.reify_term t \ declare[[ML_print_depth = 30]] ML\ val t = Proofterm.combination_axm -val tt = ISA_core.reify_proofterm t +val tt = Meta_ISA_core.reify_proofterm t (*val ttt = Value_Command.value \<^context> tt*) \ @@ -218,8 +218,8 @@ proof_tag :: int <= "1" text*[instance_test::class_test, proof_tag = "2"]\\ -term*\proof_tag @{class-test \instance_test\}\ -value*\proof_tag @{class-test \instance_test\}\ +term*\proof_tag @{class_test \instance_test\}\ +value*\proof_tag @{class_test \instance_test\}\ ML\ val t = @{thm "refl"} @@ -264,21 +264,21 @@ value*\proof @{thm \four_is_even\}\ ML\val t = Proofterm.equal_elim_axm\ ML\ -val tt = ISA_core.reify_proofterm t +val tt = Meta_ISA_core.reify_proofterm t \ -term*\@{term \proof_tag @{class-test \instance_test\}\}\ +term*\@{term \proof_tag @{class_test \instance_test\}\}\ -value*\@{term \proof_tag @{class-test \instance_test\}\}\ +value*\@{term \proof_tag @{class_test \instance_test\}\}\ fun* pattern where "pattern (PAxm ((Ct a (Ty ba [constT bb, (Ty bc [constT bd, constT be])])) $ c $ d) [((Var e, f), constT g), ((Var h, i), j)]) = (if be = STR ''prop'' then (Appt (PAxm ((Ct a (Ty ba [constT bb, (Ty bc [constT bd, constT be])])) $ c $ d) [((Var e, f), constT g), ((Var h, i), j)]) - (@{term \proof_tag @{class-test \instance_test\}\})) + (@{term \proof_tag @{class_test \instance_test\}\})) else (PAxm ((Ct a (Ty ba [constT bb, (Ty bc [constT bd, constT be])])) $ c $ d) [((Var e, f), constT g), ((Var h, i), j)]))" | "pattern x = x" @@ -317,8 +317,8 @@ term\ term\(constT b \ (constT b \ constT b))\ term\Ty STR ''fun'' [(Ty STR ''fun'' [constT b, constT b]), constT b]\ ML\ -val t = \<^value_>\@{class-test \instance_test\}\ -val tt = ISA_core.reify_term t +val t = \<^value_>\@{class_test \instance_test\}\ +val tt = Meta_ISA_core.reify_term t \ (*fun* pattern where*) @@ -337,15 +337,15 @@ val t = \<^value_>\pattern (PAxm (mk_eq' propT Core.A Core.B \ \*) ML\\ -fun* get_proof where +(*fun* get_proof where "get_proof Appt ((PAxm ((Ct a (Ty ba [constT bb, (Ty bc [constT bd, constT be])])) $ c $ d) [((Var e, f), constT g), ((Var h, i), j)])) (Ct _) = (if be = STR ''prop'' then (Appt (PAxm ((Ct a (Ty ba [constT bb, (Ty bc [constT bd, constT be])])) $ c $ d) [((Var e, f), constT g), ((Var h, i), j)]) - (@{term \@{class-test \instance_test\}\})) + (@{term \@{class_test \instance_test\}\})) else (PAxm ((Ct a (Ty ba [constT bb, (Ty bc [constT bd, constT be])])) $ c $ d) [((Var e, f), constT g), ((Var h, i), j)]))" (*| "pattern x = (Appt x (@{term \@{cc-assumption-test \cc_assumption_test_ref\}\}))"*) -| "get_proof x = x" +| "get_proof x = x"*) (*fun* pattern' where "pattern' (AppP diff --git a/Isabelle_DOF-Proofs/fun.ML b/Isabelle_DOF-Proofs/fun.ML index f8b87df2..11d314fa 100644 --- a/Isabelle_DOF-Proofs/fun.ML +++ b/Isabelle_DOF-Proofs/fun.ML @@ -170,7 +170,7 @@ fun add_fun_cmd a b c int = gen_add_fun (fn tac => Function.add_function_cmd a b -val _ = +val _ = Outer_Syntax.local_theory' \<^command_keyword>\fun*\ "define general recursive functions (short version)" (function_parser fun_config diff --git a/Isabelle_DOF-Proofs/function.ML b/Isabelle_DOF-Proofs/function.ML index 51768c51..7a992509 100644 --- a/Isabelle_DOF-Proofs/function.ML +++ b/Isabelle_DOF-Proofs/function.ML @@ -129,7 +129,7 @@ fun prepare_function do_print prep fixspec eqns config lthy = (K false) (map fst fixes) in (info, - lthy2 |> Local_Theory.declaration {syntax = false, pervasive = false} + lthy2 |> Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>} (fn phi => add_function_data (transform_function_data phi info))) end in @@ -209,7 +209,7 @@ fun prepare_termination_proof prep_binding prep_term raw_term_opt lthy = in (info', lthy2 - |> Local_Theory.declaration {syntax = false, pervasive = false} + |> Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>} (fn phi => add_function_data (transform_function_data phi info')) |> Spec_Rules.add Binding.empty Spec_Rules.equational_recdef fs tsimps) end) diff --git a/Isabelle_DOF-Proofs/specification.ML b/Isabelle_DOF-Proofs/specification.ML index e3689ba4..4269aef2 100644 --- a/Isabelle_DOF-Proofs/specification.ML +++ b/Isabelle_DOF-Proofs/specification.ML @@ -260,21 +260,19 @@ fun gen_def prep_spec prep_att raw_var raw_params raw_prems ((a, raw_atts), raw_ val ((lhs, (_, raw_th)), lthy2) = lthy |> Local_Theory.define_internal ((b, mx), ((Binding.suffix_name "_raw" name, []), rhs)); - val th = prove lthy2 raw_th; - val lthy3 = lthy2 |> Spec_Rules.add name Spec_Rules.equational [lhs] [th]; + val ([(def_name, [th])], lthy3) = lthy2 + |> Local_Theory.notes [((name, atts), [([prove lthy2 raw_th], [])])]; - val ([(def_name, [th'])], lthy4) = lthy3 - |> Local_Theory.notes [((name, atts), [([th], [])])]; + val lthy4 = lthy3 + |> Spec_Rules.add name Spec_Rules.equational [lhs] [th] + |> Code.declare_default_eqns [(th, true)]; - val lthy5 = lthy4 - |> Code.declare_default_eqns [(th', true)]; - - val lhs' = Morphism.term (Local_Theory.target_morphism lthy5) lhs; + val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs; val _ = - Proof_Display.print_consts int (Position.thread_data ()) lthy5 + Proof_Display.print_consts int (Position.thread_data ()) lthy4 (Frees.defined (Frees.build (Frees.add_frees lhs'))) [(x, T)]; - in ((lhs, (def_name, th')), lthy5) end; + in ((lhs, (def_name, th)), lthy4) end; fun definition xs ys As B = gen_def check_spec_open (K I) xs ys As B false; val definition_cmd = gen_def read_spec_open Attrib.check_src; @@ -346,7 +344,10 @@ fun gen_theorems prep_fact prep_att add_fixes |> Attrib.partial_evaluation ctxt' |> Attrib.transform_facts (Proof_Context.export_morphism ctxt' lthy); val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts'; - val _ = Proof_Display.print_results int (Position.thread_data ()) lthy' ((kind, ""), res); + val _ = + Proof_Display.print_results + {interactive = int, pos = Position.thread_data (), proof_state = false} + lthy' ((kind, ""), res); in (res, lthy') end; in @@ -399,6 +400,9 @@ fun gen_theorem schematic bundle_includes prep_att prep_stmt val atts = more_atts @ map (prep_att lthy) raw_atts; val pos = Position.thread_data (); + val print_results = + Proof_Display.print_results {interactive = int, pos = pos, proof_state = false}; + fun after_qed' results goal_ctxt' = let val results' = @@ -409,13 +413,13 @@ fun gen_theorem schematic bundle_includes prep_att prep_stmt Local_Theory.notes_kind kind (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy; val lthy'' = - if Binding.is_empty_atts (name, atts) then - (Proof_Display.print_results int pos lthy' ((kind, ""), res); lthy') + if Binding.is_empty_atts (name, atts) + then (print_results lthy' ((kind, ""), res); lthy') else let val ([(res_name, _)], lthy'') = Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])] lthy'; - val _ = Proof_Display.print_results int pos lthy' ((kind, res_name), res); + val _ = print_results lthy' ((kind, res_name), res); in lthy'' end; in after_qed results' lthy'' end;