nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Update dedukti-presentation example to Isabelle 2023

This commit is contained in:
Nicolas Méric 2023-10-10 09:54:49 +02:00
parent 989ab3c315
commit fda02be889
4 changed files with 34 additions and 30 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
Isabelle_DOF-Proofs/Reification_Test.thy
View File

@ -178,12 +178,12 @@ ML\<open>
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
\<close>
declare[[ML_print_depth = 30]]
ML\<open>
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*)
\<close>
@ -218,8 +218,8 @@ proof_tag :: int <= "1"
text*[instance_test::class_test, proof_tag = "2"]\<open>\<close>
term*\<open>proof_tag @{class-test \<open>instance_test\<close>}\<close>
value*\<open>proof_tag @{class-test \<open>instance_test\<close>}\<close>
term*\<open>proof_tag @{class_test \<open>instance_test\<close>}\<close>
value*\<open>proof_tag @{class_test \<open>instance_test\<close>}\<close>
ML\<open>
val t = @{thm "refl"}
@ -264,21 +264,21 @@ value*\<open>proof @{thm \<open>four_is_even\<close>}\<close>
ML\<open>val t = Proofterm.equal_elim_axm\<close>
ML\<open>
val tt = ISA_core.reify_proofterm t
val tt = Meta_ISA_core.reify_proofterm t
\<close>
term*\<open>@{term \<open>proof_tag @{class-test \<open>instance_test\<close>}\<close>}\<close>
term*\<open>@{term \<open>proof_tag @{class_test \<open>instance_test\<close>}\<close>}\<close>
value*\<open>@{term \<open>proof_tag @{class-test \<open>instance_test\<close>}\<close>}\<close>
value*\<open>@{term \<open>proof_tag @{class_test \<open>instance_test\<close>}\<close>}\<close>
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 \<open>proof_tag @{class-test \<open>instance_test\<close>}\<close>}))
(@{term \<open>proof_tag @{class_test \<open>instance_test\<close>}\<close>}))
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\<open>
term\<open>(constT b \<rightarrow> (constT b \<rightarrow> constT b))\<close>
term\<open>Ty STR ''fun'' [(Ty STR ''fun'' [constT b, constT b]), constT b]\<close>
ML\<open>
val t = \<^value_>\<open>@{class-test \<open>instance_test\<close>}\<close>
val tt = ISA_core.reify_term t
val t = \<^value_>\<open>@{class_test \<open>instance_test\<close>}\<close>
val tt = Meta_ISA_core.reify_term t
\<close>
(*fun* pattern where*)
@ -337,15 +337,15 @@ val t = \<^value_>\<open>pattern (PAxm (mk_eq' propT Core.A Core.B \<longmapsto>
\<close>*)
ML\<open>\<close>
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 \<open>@{class-test \<open>instance_test\<close>}\<close>}))
(@{term \<open>@{class_test \<open>instance_test\<close>}\<close>}))
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 \<open>@{cc-assumption-test \<open>cc_assumption_test_ref\<close>}\<close>}))"*)
| "get_proof x = x"
| "get_proof x = x"*)
(*fun* pattern' where
"pattern' (AppP

2
Isabelle_DOF-Proofs/fun.ML
View File

@ -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>\<open>fun*\<close>
"define general recursive functions (short version)"
(function_parser fun_config

4
Isabelle_DOF-Proofs/function.ML
View File

@ -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)

32
Isabelle_DOF-Proofs/specification.ML
View File

@ -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;