author | wenzelm |
Fri, 15 Oct 2021 19:25:31 +0200 | |
changeset 74525 | c960bfcb91db |
parent 70225 | 129757af1096 |
child 78820 | b356019e8d49 |
permissions | -rw-r--r-- |
70018
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
1 |
(* Title: HOL/ex/Sketch_and_Explore.thy |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
2 |
Author: Florian Haftmann, TU Muenchen |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
3 |
*) |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
4 |
|
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
5 |
chapter \<open>Experimental commands \<^text>\<open>sketch\<close> and \<^text>\<open>explore\<close>\<close> |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
6 |
|
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
7 |
theory Sketch_and_Explore |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
8 |
imports Main \<comment> \<open>TODO: generalize existing sledgehammer functions to Pure\<close> |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
9 |
keywords "sketch" "explore" :: diag |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
10 |
begin |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
11 |
|
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
12 |
ML \<open> |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
13 |
fun split_clause t = |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
14 |
let |
74525
c960bfcb91db
discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;
wenzelm
parents:
70225
diff
changeset
|
15 |
val (fixes, horn) = funpow_yield (length (Term.strip_all_vars t)) Logic.dest_all_global t; |
70018
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
16 |
val assms = Logic.strip_imp_prems horn; |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
17 |
val concl = Logic.strip_imp_concl horn; |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
18 |
in (fixes, assms, concl) end; |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
19 |
|
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
20 |
fun maybe_quote ctxt = |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
21 |
ATP_Util.maybe_quote (Thy_Header.get_keywords' ctxt); |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
22 |
|
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
23 |
fun print_typ ctxt T = |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
24 |
T |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
25 |
|> Syntax.string_of_typ ctxt |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
26 |
|> maybe_quote ctxt; |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
27 |
|
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
28 |
fun print_term ctxt t = |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
29 |
t |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
30 |
|> singleton (Syntax.uncheck_terms ctxt) |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
31 |
|> Sledgehammer_Isar_Annotate.annotate_types_in_term ctxt |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
32 |
\<comment> \<open>TODO pointless to annotate explicit fixes in term\<close> |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
33 |
|> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of) |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
34 |
|> Sledgehammer_Util.simplify_spaces |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
35 |
|> maybe_quote ctxt; |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
36 |
|
70225
129757af1096
more correct simulation of eigen context for generated Isar statements
haftmann
parents:
70018
diff
changeset
|
37 |
fun eigen_context_for_statement (fixes, assms, concl) ctxt = |
70018
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
38 |
let |
70225
129757af1096
more correct simulation of eigen context for generated Isar statements
haftmann
parents:
70018
diff
changeset
|
39 |
val (fixes', ctxt') = Variable.add_fixes (map fst fixes) ctxt; |
129757af1096
more correct simulation of eigen context for generated Isar statements
haftmann
parents:
70018
diff
changeset
|
40 |
val subst_free = AList.lookup (op =) (map fst fixes ~~ fixes') |
129757af1096
more correct simulation of eigen context for generated Isar statements
haftmann
parents:
70018
diff
changeset
|
41 |
val subst = map_aterms (fn Free (v, T) => Free (the_default v (subst_free v), T) |
129757af1096
more correct simulation of eigen context for generated Isar statements
haftmann
parents:
70018
diff
changeset
|
42 |
| t => t) |
129757af1096
more correct simulation of eigen context for generated Isar statements
haftmann
parents:
70018
diff
changeset
|
43 |
val assms' = map subst assms; |
129757af1096
more correct simulation of eigen context for generated Isar statements
haftmann
parents:
70018
diff
changeset
|
44 |
val concl' = subst concl; |
129757af1096
more correct simulation of eigen context for generated Isar statements
haftmann
parents:
70018
diff
changeset
|
45 |
in ((fixes, assms', concl'), ctxt') end; |
129757af1096
more correct simulation of eigen context for generated Isar statements
haftmann
parents:
70018
diff
changeset
|
46 |
|
129757af1096
more correct simulation of eigen context for generated Isar statements
haftmann
parents:
70018
diff
changeset
|
47 |
fun print_isar_skeleton ctxt indent keyword stmt = |
129757af1096
more correct simulation of eigen context for generated Isar statements
haftmann
parents:
70018
diff
changeset
|
48 |
let |
129757af1096
more correct simulation of eigen context for generated Isar statements
haftmann
parents:
70018
diff
changeset
|
49 |
val ((fixes, assms, concl), ctxt') = eigen_context_for_statement stmt ctxt; |
70018
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
50 |
val prefix = replicate_string indent " "; |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
51 |
\<comment> \<open>TODO consider pre-existing indentation -- how?\<close> |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
52 |
val prefix_sep = "\n" ^ prefix ^ " and "; |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
53 |
val show_s = prefix ^ keyword ^ " " ^ print_term ctxt' concl; |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
54 |
val if_s = if null assms then NONE |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
55 |
else SOME (prefix ^ " if " ^ space_implode prefix_sep |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
56 |
(map (print_term ctxt') assms)); |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
57 |
val for_s = if null fixes then NONE |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
58 |
else SOME (prefix ^ " for " ^ space_implode prefix_sep |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
59 |
(map (fn (v, T) => v ^ " :: " ^ print_typ ctxt T) fixes)); |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
60 |
val s = cat_lines ([show_s] @ map_filter I [if_s, for_s] @ |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
61 |
[prefix ^ " " ^ (if is_none if_s then "" else "using that ") ^ "sorry"]); |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
62 |
in |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
63 |
s |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
64 |
end; |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
65 |
|
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
66 |
fun print_sketch ctxt method_text clauses = |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
67 |
"proof" ^ method_text :: map (print_isar_skeleton ctxt 2 "show") clauses @ ["qed"]; |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
68 |
|
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
69 |
fun print_exploration ctxt method_text [clause] = |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
70 |
["proof -", print_isar_skeleton ctxt 2 "have" clause, |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
71 |
" then show ?thesis", " by" ^ method_text, "qed"] |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
72 |
| print_exploration ctxt method_text (clause :: clauses) = |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
73 |
"proof -" :: print_isar_skeleton ctxt 2 "have" clause |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
74 |
:: map (print_isar_skeleton ctxt 2 "moreover have") clauses |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
75 |
@ [" ultimately show ?thesis", " by" ^ method_text, "qed"]; |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
76 |
|
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
77 |
fun coalesce_method_txt [] = "" |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
78 |
| coalesce_method_txt [s] = s |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
79 |
| coalesce_method_txt (s1 :: s2 :: ss) = |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
80 |
if s1 = "(" orelse s1 = "[" |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
81 |
orelse s2 = ")" orelse s2 = "]" orelse s2= ":" |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
82 |
then s1 ^ coalesce_method_txt (s2 :: ss) |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
83 |
else s1 ^ " " ^ coalesce_method_txt (s2 :: ss); |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
84 |
|
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
85 |
fun print_proof_text_from_state print (some_method_ref : ((Method.text * Position.range) * Token.T list) option) state = |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
86 |
let |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
87 |
val state' = state |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
88 |
|> Proof.proof (Option.map fst some_method_ref) |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
89 |
|> Seq.the_result "" |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
90 |
|
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
91 |
val { context = ctxt, facts = _, goal } = Proof.goal state'; |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
92 |
|
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
93 |
val ctxt_print = fold (fn opt => Config.put opt false) |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
94 |
[show_markup, Printer.show_type_emphasis, show_types, show_sorts, show_consts] ctxt |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
95 |
|
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
96 |
val method_text = case some_method_ref of |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
97 |
NONE => "" |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
98 |
| SOME (_, toks) => " " ^ coalesce_method_txt (map Token.unparse toks); |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
99 |
\<comment> \<open>TODO proper printing required\<close> |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
100 |
val goal_props = Logic.strip_imp_prems (Thm.prop_of goal); |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
101 |
val clauses = map split_clause goal_props; |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
102 |
val lines = if null clauses then |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
103 |
if is_none some_method_ref then [" .."] |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
104 |
else [" by" ^ method_text] |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
105 |
else print ctxt_print method_text clauses; |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
106 |
val message = Active.sendback_markup_properties [] (cat_lines lines); |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
107 |
in |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
108 |
(state |> tap (fn _ => Output.information message)) |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
109 |
end |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
110 |
|
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
111 |
val sketch = print_proof_text_from_state print_sketch; |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
112 |
|
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
113 |
fun explore method_ref = print_proof_text_from_state print_exploration (SOME method_ref); |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
114 |
|
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
115 |
fun sketch_cmd some_method_text = |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
116 |
Toplevel.keep_proof (K () o sketch some_method_text o Toplevel.proof_of) |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
117 |
|
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
118 |
fun explore_cmd method_text = |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
119 |
Toplevel.keep_proof (K () o explore method_text o Toplevel.proof_of) |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
120 |
|
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
121 |
val _ = |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
122 |
Outer_Syntax.command \<^command_keyword>\<open>sketch\<close> |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
123 |
"print sketch of Isar proof text after method application" |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
124 |
(Scan.option (Scan.trace Method.parse) >> sketch_cmd); |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
125 |
|
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
126 |
val _ = |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
127 |
Outer_Syntax.command \<^command_keyword>\<open>explore\<close> |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
128 |
"explore proof obligations after method application as Isar proof text" |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
129 |
(Scan.trace Method.parse >> explore_cmd); |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
130 |
\<close> |
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
131 |
|
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
diff
changeset
|
132 |
end |