author | wenzelm |
Fri, 04 Mar 2022 23:22:39 +0100 | |
changeset 75215 | 1129e82dc1ec |
parent 74365 | b49bd5d9041f |
child 76074 | 2456721602b2 |
permissions | -rw-r--r-- |
74365
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/ex/Guess.thy |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
3 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
4 |
Improper proof command 'guess': variant of 'obtain' based on tactical result. |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
5 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
6 |
<chain_facts> |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
7 |
guess x <proof body> <proof end> \<equiv> |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
8 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
9 |
{ |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
10 |
fix thesis |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
11 |
<chain_facts> have "PROP ?guess" |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
12 |
apply magic \<comment> \<open>turn goal into \<open>thesis \<Longrightarrow> #thesis\<close>\<close> |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
13 |
<proof body> |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
14 |
apply_end magic \<comment> \<open>turn final \<open>(\<And>x. P x \<Longrightarrow> thesis) \<Longrightarrow> #thesis\<close> into\<close> |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
15 |
\<comment> \<open>\<open>#((\<And>x. A x \<Longrightarrow> thesis) \<Longrightarrow> thesis)\<close> which is a finished goal state\<close> |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
16 |
<proof end> |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
17 |
} |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
18 |
fix x assm <<obtain_export>> "A x" |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
19 |
*) |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
20 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
21 |
section \<open>Improper proof command 'guess'\<close> |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
22 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
23 |
theory Guess |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
24 |
imports Pure |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
25 |
keywords "guess" :: prf_script_asm_goal % "proof" |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
26 |
begin |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
27 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
28 |
text \<open> |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
29 |
The @{command guess} is similar to @{command obtain}, but it derives the |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
30 |
obtained context elements from the course of tactical reasoning in the |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
31 |
proof. Thus it can considerably obscure the proof: it is provided here as |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
32 |
\<^emph>\<open>improper\<close> and experimental feature. |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
33 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
34 |
A proof with @{command guess} starts with a fixed goal \<open>thesis\<close>. The |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
35 |
subsequent refinement steps may turn this to anything of the form |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
36 |
\<open>\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis\<close>, but without splitting into new |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
37 |
subgoals. The final goal state is then used as reduction rule for the obtain |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
38 |
pattern described above. Obtained parameters \<open>\<^vec>x\<close> are marked as |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
39 |
internal by default, and thus inaccessible in the proof text. The variable |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
40 |
names and type constraints given as arguments for @{command "guess"} specify |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
41 |
a prefix of accessible parameters. |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
42 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
43 |
Some examples are in \<^file>\<open>Guess_Examples.thy\<close>. |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
44 |
\<close> |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
45 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
46 |
ML \<open> |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
47 |
signature GUESS = |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
48 |
sig |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
49 |
val guess: (binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
50 |
val guess_cmd: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
51 |
end; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
52 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
53 |
structure Guess: GUESS = |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
54 |
struct |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
55 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
56 |
local |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
57 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
58 |
fun unify_params vars thesis_var raw_rule ctxt = |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
59 |
let |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
60 |
val thy = Proof_Context.theory_of ctxt; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
61 |
val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt); |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
62 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
63 |
fun err msg th = error (msg ^ ":\n" ^ Thm.string_of_thm ctxt th); |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
64 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
65 |
val maxidx = fold (Term.maxidx_typ o snd o fst) vars ~1; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
66 |
val rule = Thm.incr_indexes (maxidx + 1) raw_rule; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
67 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
68 |
val params = Rule_Cases.strip_params (Logic.nth_prem (1, Thm.prop_of rule)); |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
69 |
val m = length vars; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
70 |
val n = length params; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
71 |
val _ = m <= n orelse err "More variables than parameters in obtained rule" rule; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
72 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
73 |
fun unify ((x, T), (y, U)) (tyenv, max) = Sign.typ_unify thy (T, U) (tyenv, max) |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
74 |
handle Type.TUNIFY => |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
75 |
err ("Failed to unify variable " ^ |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
76 |
string_of_term (Free (x, Envir.norm_type tyenv T)) ^ " against parameter " ^ |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
77 |
string_of_term (Syntax_Trans.mark_bound_abs (y, Envir.norm_type tyenv U)) ^ " in") rule; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
78 |
val (tyenv, _) = fold unify (map #1 vars ~~ take m params) |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
79 |
(Vartab.empty, Int.max (maxidx, Thm.maxidx_of rule)); |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
80 |
val norm_type = Envir.norm_type tyenv; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
81 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
82 |
val xs = map (apsnd norm_type o fst) vars; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
83 |
val ys = map (apsnd norm_type) (drop m params); |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
84 |
val ys' = map Name.internal (Name.variant_list (map fst xs) (map fst ys)) ~~ map #2 ys; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
85 |
val terms = map (Drule.mk_term o Thm.cterm_of ctxt o Free) (xs @ ys'); |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
86 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
87 |
val instT = |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
88 |
TVars.build |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
89 |
(params |> fold (#2 #> Term.fold_atyps (fn T => fn instT => |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
90 |
(case T of |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
91 |
TVar v => |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
92 |
if TVars.defined instT v then instT |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
93 |
else TVars.add (v, Thm.ctyp_of ctxt (norm_type T)) instT |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
94 |
| _ => instT)))); |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
95 |
val closed_rule = rule |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
96 |
|> Thm.forall_intr (Thm.cterm_of ctxt (Free thesis_var)) |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
97 |
|> Thm.instantiate (instT, Vars.empty); |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
98 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
99 |
val ((_, rule' :: terms'), ctxt') = Variable.import false (closed_rule :: terms) ctxt; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
100 |
val vars' = |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
101 |
map (dest_Free o Thm.term_of o Drule.dest_term) terms' ~~ |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
102 |
(map snd vars @ replicate (length ys) NoSyn); |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
103 |
val rule'' = Thm.forall_elim (Thm.cterm_of ctxt' (Logic.varify_global (Free thesis_var))) rule'; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
104 |
in ((vars', rule''), ctxt') end; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
105 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
106 |
fun inferred_type (binding, _, mx) ctxt = |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
107 |
let |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
108 |
val x = Variable.check_name binding; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
109 |
val ((_, T), ctxt') = Proof_Context.inferred_param x ctxt |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
110 |
in ((x, T, mx), ctxt') end; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
111 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
112 |
fun polymorphic ctxt vars = |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
113 |
let val Ts = map Logic.dest_type (Variable.polymorphic ctxt (map (Logic.mk_type o #2) vars)) |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
114 |
in map2 (fn (x, _, mx) => fn T => ((x, T), mx)) vars Ts end; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
115 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
116 |
fun gen_guess prep_var raw_vars int state = |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
117 |
let |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
118 |
val _ = Proof.assert_forward_or_chain state; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
119 |
val ctxt = Proof.context_of state; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
120 |
val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else []; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
121 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
122 |
val (thesis_var, thesis) = #1 (Obtain.obtain_thesis ctxt); |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
123 |
val vars = ctxt |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
124 |
|> fold_map prep_var raw_vars |-> fold_map inferred_type |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
125 |
|> fst |> polymorphic ctxt; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
126 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
127 |
fun guess_context raw_rule state' = |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
128 |
let |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
129 |
val ((parms, rule), ctxt') = |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
130 |
unify_params vars thesis_var raw_rule (Proof.context_of state'); |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
131 |
val (xs, _) = Variable.add_fixes (map (#1 o #1) parms) ctxt'; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
132 |
val ps = xs ~~ map (#2 o #1) parms; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
133 |
val ts = map Free ps; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
134 |
val asms = |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
135 |
Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule)) |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
136 |
|> map (fn asm => (Term.betapplys (fold_rev Term.abs ps asm, ts), [])); |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
137 |
val _ = not (null asms) orelse error "Trivial result -- nothing guessed"; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
138 |
in |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
139 |
state' |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
140 |
|> Proof.map_context (K ctxt') |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
141 |
|> Proof.fix (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms) |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
142 |
|> `Proof.context_of |-> (fn fix_ctxt => Proof.assm |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
143 |
(Obtain.obtain_export fix_ctxt rule (map (Thm.cterm_of ctxt) ts)) |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
144 |
[] [] [(Binding.empty_atts, asms)]) |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
145 |
|> Proof.map_context (fold Variable.unbind_term Auto_Bind.no_facts) |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
146 |
end; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
147 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
148 |
val goal = Var (("guess", 0), propT); |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
149 |
val pos = Position.thread_data (); |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
150 |
fun print_result ctxt' (k, [(s, [_, th])]) = |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
151 |
Proof_Display.print_results int pos ctxt' (k, [(s, [th])]); |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
152 |
val before_qed = |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
153 |
Method.primitive_text (fn ctxt => |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
154 |
Goal.conclude #> Raw_Simplifier.norm_hhf ctxt #> |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
155 |
(fn th => Goal.protect 0 (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))); |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
156 |
fun after_qed (result_ctxt, results) state' = |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
157 |
let val [_, res] = Proof_Context.export result_ctxt (Proof.context_of state') (flat results) |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
158 |
in |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
159 |
state' |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
160 |
|> Proof.end_block |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
161 |
|> guess_context (Obtain.check_result ctxt thesis res) |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
162 |
end; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
163 |
in |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
164 |
state |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
165 |
|> Proof.enter_forward |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
166 |
|> Proof.begin_block |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
167 |
|> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)] |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
168 |
|> Proof.chain_facts chain_facts |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
169 |
|> Proof.internal_goal print_result Proof_Context.mode_schematic true "guess" |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
170 |
(SOME before_qed) after_qed |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
171 |
[] [] [(Binding.empty_atts, [(Logic.mk_term goal, []), (goal, [])])] |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
172 |
|> snd |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
173 |
|> Proof.refine_singleton |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
174 |
(Method.primitive_text (fn _ => fn _ => Goal.init (Thm.cterm_of ctxt thesis))) |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
175 |
end; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
176 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
177 |
in |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
178 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
179 |
val guess = gen_guess Proof_Context.cert_var; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
180 |
val guess_cmd = gen_guess Proof_Context.read_var; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
181 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
182 |
val _ = |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
183 |
Outer_Syntax.command \<^command_keyword>\<open>guess\<close> "wild guessing (unstructured)" |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
184 |
(Scan.optional Parse.vars [] >> (Toplevel.proof' o guess_cmd)); |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
185 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
186 |
end; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
187 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
188 |
end; |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
189 |
\<close> |
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
190 |
|
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
wenzelm
parents:
diff
changeset
|
191 |
end |