author | paulson <lp15@cam.ac.uk> |
Mon, 29 Apr 2019 17:11:26 +0100 | |
changeset 70214 | 58191e01f0b1 |
parent 69597 | ff784d5a5bfb |
child 74395 | 5399dfe9141c |
permissions | -rw-r--r-- |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
1 |
(* Title: HOL/ex/veriT_Preprocessing.thy |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
2 |
Author: Jasmin Christian Blanchette, Inria, LORIA, MPII |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
3 |
*) |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
4 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
5 |
section \<open>Proof Reconstruction for veriT's Preprocessing\<close> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
6 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
7 |
theory veriT_Preprocessing |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
8 |
imports Main |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
9 |
begin |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
10 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
11 |
declare [[eta_contract = false]] |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
12 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
13 |
lemma |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
14 |
some_All_iffI: "p (SOME x. \<not> p x) = q \<Longrightarrow> (\<forall>x. p x) = q" and |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
15 |
some_Ex_iffI: "p (SOME x. p x) = q \<Longrightarrow> (\<exists>x. p x) = q" |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
16 |
by (metis (full_types) someI_ex)+ |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
17 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
18 |
ML \<open> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
19 |
fun mk_prod1 bound_Ts (t, u) = |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
20 |
HOLogic.pair_const (fastype_of1 (bound_Ts, t)) (fastype_of1 (bound_Ts, u)) $ t $ u; |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
21 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
22 |
fun mk_tuple1 bound_Ts = the_default HOLogic.unit o try (foldr1 (mk_prod1 bound_Ts)); |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
23 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
24 |
fun mk_arg_congN 0 = refl |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
25 |
| mk_arg_congN 1 = arg_cong |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
26 |
| mk_arg_congN 2 = @{thm arg_cong2} |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
27 |
| mk_arg_congN n = arg_cong RS funpow (n - 2) (fn th => @{thm cong} RS th) @{thm cong}; |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
28 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
29 |
fun mk_let_iffNI ctxt n = |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
30 |
let |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
31 |
val ((As, [B]), _) = ctxt |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
32 |
|> Ctr_Sugar_Util.mk_TFrees n |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
33 |
||>> Ctr_Sugar_Util.mk_TFrees 1; |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
34 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
35 |
val ((((ts, us), [p]), [q]), _) = ctxt |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
36 |
|> Ctr_Sugar_Util.mk_Frees "t" As |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
37 |
||>> Ctr_Sugar_Util.mk_Frees "u" As |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
38 |
||>> Ctr_Sugar_Util.mk_Frees "p" [As ---> B] |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
39 |
||>> Ctr_Sugar_Util.mk_Frees "q" [B]; |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
40 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
41 |
val tuple_t = HOLogic.mk_tuple ts; |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
42 |
val tuple_T = fastype_of tuple_t; |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
43 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
44 |
val lambda_t = HOLogic.tupled_lambda tuple_t (list_comb (p, ts)); |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
45 |
val lambda_T = fastype_of lambda_t; |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
46 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
47 |
val left_prems = map2 (curry Ctr_Sugar_Util.mk_Trueprop_eq) ts us; |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
48 |
val right_prem = Ctr_Sugar_Util.mk_Trueprop_eq (list_comb (p, us), q); |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
49 |
val concl = Ctr_Sugar_Util.mk_Trueprop_eq |
69597 | 50 |
(Const (\<^const_name>\<open>Let\<close>, tuple_T --> lambda_T --> B) $ tuple_t $ lambda_t, q); |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
51 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
52 |
val goal = Logic.list_implies (left_prems @ [right_prem], concl); |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
53 |
val vars = Variable.add_free_names ctxt goal []; |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
54 |
in |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
55 |
Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, ...} => |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
56 |
HEADGOAL (hyp_subst_tac ctxt) THEN |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
57 |
Local_Defs.unfold0_tac ctxt @{thms Let_def prod.case} THEN |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
58 |
HEADGOAL (resolve_tac ctxt [refl])) |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
59 |
end; |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
60 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
61 |
datatype rule_name = |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
62 |
Refl |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
63 |
| Taut of thm |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
64 |
| Trans of term |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
65 |
| Cong |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
66 |
| Bind |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
67 |
| Sko_Ex |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
68 |
| Sko_All |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
69 |
| Let of term list; |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
70 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
71 |
fun str_of_rule_name Refl = "Refl" |
69597 | 72 |
| str_of_rule_name (Taut th) = "Taut[" ^ \<^make_string> th ^ "]" |
73 |
| str_of_rule_name (Trans t) = "Trans[" ^ Syntax.string_of_term \<^context> t ^ "]" |
|
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
74 |
| str_of_rule_name Cong = "Cong" |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
75 |
| str_of_rule_name Bind = "Bind" |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
76 |
| str_of_rule_name Sko_Ex = "Sko_Ex" |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
77 |
| str_of_rule_name Sko_All = "Sko_All" |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
78 |
| str_of_rule_name (Let ts) = |
69597 | 79 |
"Let[" ^ commas (map (Syntax.string_of_term \<^context>) ts) ^ "]"; |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
80 |
|
65017 | 81 |
datatype node = N of rule_name * node list; |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
82 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
83 |
fun lambda_count (Abs (_, _, t)) = lambda_count t + 1 |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
84 |
| lambda_count ((t as Abs _) $ _) = lambda_count t - 1 |
69597 | 85 |
| lambda_count ((t as Const (\<^const_name>\<open>case_prod\<close>, _) $ _) $ _) = lambda_count t - 1 |
86 |
| lambda_count (Const (\<^const_name>\<open>case_prod\<close>, _) $ t) = lambda_count t - 1 |
|
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
87 |
| lambda_count _ = 0; |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
88 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
89 |
fun zoom apply = |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
90 |
let |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
91 |
fun zo 0 bound_Ts (Abs (r, T, t), Abs (s, U, u)) = |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
92 |
let val (t', u') = zo 0 (T :: bound_Ts) (t, u) in |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
93 |
(lambda (Free (r, T)) t', lambda (Free (s, U)) u') |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
94 |
end |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
95 |
| zo 0 bound_Ts ((t as Abs (_, T, _)) $ arg, u) = |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
96 |
let val (t', u') = zo 1 (T :: bound_Ts) (t, u) in |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
97 |
(t' $ arg, u') |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
98 |
end |
69597 | 99 |
| zo 0 bound_Ts ((t as Const (\<^const_name>\<open>case_prod\<close>, _) $ _) $ arg, u) = |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
100 |
let val (t', u') = zo 1 bound_Ts (t, u) in |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
101 |
(t' $ arg, u') |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
102 |
end |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
103 |
| zo 0 bound_Ts tu = apply bound_Ts tu |
69597 | 104 |
| zo n bound_Ts (Const (\<^const_name>\<open>case_prod\<close>, |
105 |
Type (\<^type_name>\<open>fun\<close>, [Type (\<^type_name>\<open>fun\<close>, [A, Type (\<^type_name>\<open>fun\<close>, [B, _])]), |
|
106 |
Type (\<^type_name>\<open>fun\<close>, [AB, _])])) $ t, u) = |
|
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
107 |
let |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
108 |
val (t', u') = zo (n + 1) bound_Ts (t, u); |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
109 |
val C = range_type (range_type (fastype_of t')); |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
110 |
in |
69597 | 111 |
(Const (\<^const_name>\<open>case_prod\<close>, (A --> B --> C) --> AB --> C) $ t', u') |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
112 |
end |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
113 |
| zo n bound_Ts (Abs (s, T, t), u) = |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
114 |
let val (t', u') = zo (n - 1) (T :: bound_Ts) (t, u) in |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
115 |
(Abs (s, T, t'), u') |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
116 |
end |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
117 |
| zo _ _ (t, u) = raise TERM ("zoom", [t, u]); |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
118 |
in |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
119 |
zo 0 [] |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
120 |
end; |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
121 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
122 |
fun apply_Trans_left t (lhs, _) = (lhs, t); |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
123 |
fun apply_Trans_right t (_, rhs) = (t, rhs); |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
124 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
125 |
fun apply_Cong ary j (lhs, rhs) = |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
126 |
(case apply2 strip_comb (lhs, rhs) of |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
127 |
((c, ts), (d, us)) => |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
128 |
if c aconv d andalso length ts = ary andalso length us = ary then (nth ts j, nth us j) |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
129 |
else raise TERM ("apply_Cong", [lhs, rhs])); |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
130 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
131 |
fun apply_Bind (lhs, rhs) = |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
132 |
(case (lhs, rhs) of |
69597 | 133 |
(Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, T, t), Const (\<^const_name>\<open>All\<close>, _) $ Abs (s, U, u)) => |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
134 |
(Abs (s, T, t), Abs (s, U, u)) |
69597 | 135 |
| (Const (\<^const_name>\<open>Ex\<close>, _) $ t, Const (\<^const_name>\<open>Ex\<close>, _) $ u) => (t, u) |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
136 |
| _ => raise TERM ("apply_Bind", [lhs, rhs])); |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
137 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
138 |
fun apply_Sko_Ex (lhs, rhs) = |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
139 |
(case lhs of |
69597 | 140 |
Const (\<^const_name>\<open>Ex\<close>, _) $ (t as Abs (_, T, _)) => |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
141 |
(t $ (HOLogic.choice_const T $ t), rhs) |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
142 |
| _ => raise TERM ("apply_Sko_Ex", [lhs])); |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
143 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
144 |
fun apply_Sko_All (lhs, rhs) = |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
145 |
(case lhs of |
69597 | 146 |
Const (\<^const_name>\<open>All\<close>, _) $ (t as Abs (s, T, body)) => |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
147 |
(t $ (HOLogic.choice_const T $ Abs (s, T, HOLogic.mk_not body)), rhs) |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
148 |
| _ => raise TERM ("apply_Sko_All", [lhs])); |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
149 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
150 |
fun apply_Let_left ts j (lhs, _) = |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
151 |
(case lhs of |
69597 | 152 |
Const (\<^const_name>\<open>Let\<close>, _) $ t $ _ => |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
153 |
let val ts0 = HOLogic.strip_tuple t in |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
154 |
(nth ts0 j, nth ts j) |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
155 |
end |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
156 |
| _ => raise TERM ("apply_Let_left", [lhs])); |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
157 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
158 |
fun apply_Let_right ts bound_Ts (lhs, rhs) = |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
159 |
let val t' = mk_tuple1 bound_Ts ts in |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
160 |
(case lhs of |
69597 | 161 |
Const (\<^const_name>\<open>Let\<close>, _) $ _ $ u => (u $ t', rhs) |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
162 |
| _ => raise TERM ("apply_Let_right", [lhs, rhs])) |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
163 |
end; |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
164 |
|
65017 | 165 |
fun reconstruct_proof ctxt (lrhs as (_, rhs), N (rule_name, prems)) = |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
166 |
let |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
167 |
val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq lrhs); |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
168 |
val ary = length prems; |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
169 |
|
69597 | 170 |
val _ = warning (Syntax.string_of_term \<^context> goal); |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
171 |
val _ = warning (str_of_rule_name rule_name); |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
172 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
173 |
val parents = |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
174 |
(case (rule_name, prems) of |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
175 |
(Refl, []) => [] |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
176 |
| (Taut _, []) => [] |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
177 |
| (Trans t, [left_prem, right_prem]) => |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
178 |
[reconstruct_proof ctxt (zoom (K (apply_Trans_left t)) lrhs, left_prem), |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
179 |
reconstruct_proof ctxt (zoom (K (apply_Trans_right t)) (rhs, rhs), right_prem)] |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
180 |
| (Cong, _) => |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
181 |
map_index (fn (j, prem) => reconstruct_proof ctxt (zoom (K (apply_Cong ary j)) lrhs, prem)) |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
182 |
prems |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
183 |
| (Bind, [prem]) => [reconstruct_proof ctxt (zoom (K apply_Bind) lrhs, prem)] |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
184 |
| (Sko_Ex, [prem]) => [reconstruct_proof ctxt (zoom (K apply_Sko_Ex) lrhs, prem)] |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
185 |
| (Sko_All, [prem]) => [reconstruct_proof ctxt (zoom (K apply_Sko_All) lrhs, prem)] |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
186 |
| (Let ts, prems) => |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
187 |
let val (left_prems, right_prem) = split_last prems in |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
188 |
map2 (fn j => fn prem => |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
189 |
reconstruct_proof ctxt (zoom (K (apply_Let_left ts j)) lrhs, prem)) |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
190 |
(0 upto length left_prems - 1) left_prems @ |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
191 |
[reconstruct_proof ctxt (zoom (apply_Let_right ts) lrhs, right_prem)] |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
192 |
end |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
193 |
| _ => raise Fail ("Invalid rule: " ^ str_of_rule_name rule_name ^ "/" ^ |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
194 |
string_of_int (length prems))); |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
195 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
196 |
val rule_thms = |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
197 |
(case rule_name of |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
198 |
Refl => [refl] |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
199 |
| Taut th => [th] |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
200 |
| Trans _ => [trans] |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
201 |
| Cong => [mk_arg_congN ary] |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
202 |
| Bind => @{thms arg_cong[of _ _ All] arg_cong[of _ _ Ex]} |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
203 |
| Sko_Ex => [@{thm some_Ex_iffI}] |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
204 |
| Sko_All => [@{thm some_All_iffI}] |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
205 |
| Let ts => [mk_let_iffNI ctxt (length ts)]); |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
206 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
207 |
val num_lams = lambda_count rhs; |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
208 |
val conged_parents = map (funpow num_lams (fn th => th RS fun_cong) |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
209 |
#> Local_Defs.unfold0 ctxt @{thms prod.case}) parents; |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
210 |
in |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
211 |
Goal.prove_sorry ctxt [] [] goal (fn {context = ctxt, ...} => |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
212 |
Local_Defs.unfold0_tac ctxt @{thms prod.case} THEN |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
213 |
HEADGOAL (REPEAT_DETERM_N num_lams o resolve_tac ctxt [ext] THEN' |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
214 |
resolve_tac ctxt rule_thms THEN' |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
215 |
K (Local_Defs.unfold0_tac ctxt @{thms prod.case}) THEN' |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
216 |
EVERY' (map (resolve_tac ctxt o single) conged_parents))) |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
217 |
end; |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
218 |
\<close> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
219 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
220 |
ML \<open> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
221 |
val proof0 = |
69597 | 222 |
((\<^term>\<open>\<exists>x :: nat. p x\<close>, |
223 |
\<^term>\<open>p (SOME x :: nat. p x)\<close>), |
|
65017 | 224 |
N (Sko_Ex, [N (Refl, [])])); |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
225 |
|
69597 | 226 |
reconstruct_proof \<^context> proof0; |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
227 |
\<close> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
228 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
229 |
ML \<open> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
230 |
val proof1 = |
69597 | 231 |
((\<^term>\<open>\<not> (\<forall>x :: nat. \<exists>y :: nat. p x y)\<close>, |
232 |
\<^term>\<open>\<not> (\<exists>y :: nat. p (SOME x :: nat. \<not> (\<exists>y :: nat. p x y)) y)\<close>), |
|
65017 | 233 |
N (Cong, [N (Sko_All, [N (Bind, [N (Refl, [])])])])); |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
234 |
|
69597 | 235 |
reconstruct_proof \<^context> proof1; |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
236 |
\<close> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
237 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
238 |
ML \<open> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
239 |
val proof2 = |
69597 | 240 |
((\<^term>\<open>\<forall>x :: nat. \<exists>y :: nat. \<exists>z :: nat. p x y z\<close>, |
241 |
\<^term>\<open>\<forall>x :: nat. p x (SOME y :: nat. \<exists>z :: nat. p x y z) |
|
242 |
(SOME z :: nat. p x (SOME y :: nat. \<exists>z :: nat. p x y z) z)\<close>), |
|
65017 | 243 |
N (Bind, [N (Sko_Ex, [N (Sko_Ex, [N (Refl, [])])])])); |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
244 |
|
69597 | 245 |
reconstruct_proof \<^context> proof2 |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
246 |
\<close> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
247 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
248 |
ML \<open> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
249 |
val proof3 = |
69597 | 250 |
((\<^term>\<open>\<forall>x :: nat. \<exists>x :: nat. \<exists>x :: nat. p x x x\<close>, |
251 |
\<^term>\<open>\<forall>x :: nat. p (SOME x :: nat. p x x x) (SOME x. p x x x) (SOME x. p x x x)\<close>), |
|
65017 | 252 |
N (Bind, [N (Sko_Ex, [N (Sko_Ex, [N (Refl, [])])])])); |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
253 |
|
69597 | 254 |
reconstruct_proof \<^context> proof3 |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
255 |
\<close> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
256 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
257 |
ML \<open> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
258 |
val proof4 = |
69597 | 259 |
((\<^term>\<open>\<forall>x :: nat. \<exists>x :: nat. \<exists>x :: nat. p x x x\<close>, |
260 |
\<^term>\<open>\<forall>x :: nat. \<exists>x :: nat. p (SOME x :: nat. p x x x) (SOME x. p x x x) (SOME x. p x x x)\<close>), |
|
65017 | 261 |
N (Bind, [N (Bind, [N (Sko_Ex, [N (Refl, [])])])])); |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
262 |
|
69597 | 263 |
reconstruct_proof \<^context> proof4 |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
264 |
\<close> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
265 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
266 |
ML \<open> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
267 |
val proof5 = |
69597 | 268 |
((\<^term>\<open>\<forall>x :: nat. q \<and> (\<exists>x :: nat. \<exists>x :: nat. p x x x)\<close>, |
269 |
\<^term>\<open>\<forall>x :: nat. q \<and> |
|
270 |
(\<exists>x :: nat. p (SOME x :: nat. p x x x) (SOME x. p x x x) (SOME x. p x x x))\<close>), |
|
65017 | 271 |
N (Bind, [N (Cong, [N (Refl, []), N (Bind, [N (Sko_Ex, [N (Refl, [])])])])])); |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
272 |
|
69597 | 273 |
reconstruct_proof \<^context> proof5 |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
274 |
\<close> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
275 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
276 |
ML \<open> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
277 |
val proof6 = |
69597 | 278 |
((\<^term>\<open>\<not> (\<forall>x :: nat. p \<and> (\<exists>x :: nat. \<forall>x :: nat. q x x))\<close>, |
279 |
\<^term>\<open>\<not> (\<forall>x :: nat. p \<and> |
|
280 |
(\<exists>x :: nat. q (SOME x :: nat. \<not> q x x) (SOME x. \<not> q x x)))\<close>), |
|
65017 | 281 |
N (Cong, [N (Bind, [N (Cong, [N (Refl, []), N (Bind, [N (Sko_All, [N (Refl, [])])])])])])); |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
282 |
|
69597 | 283 |
reconstruct_proof \<^context> proof6 |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
284 |
\<close> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
285 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
286 |
ML \<open> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
287 |
val proof7 = |
69597 | 288 |
((\<^term>\<open>\<not> \<not> (\<exists>x. p x)\<close>, |
289 |
\<^term>\<open>\<not> \<not> p (SOME x. p x)\<close>), |
|
65017 | 290 |
N (Cong, [N (Cong, [N (Sko_Ex, [N (Refl, [])])])])); |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
291 |
|
69597 | 292 |
reconstruct_proof \<^context> proof7 |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
293 |
\<close> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
294 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
295 |
ML \<open> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
296 |
val proof8 = |
69597 | 297 |
((\<^term>\<open>\<not> \<not> (let x = Suc x in x = 0)\<close>, |
298 |
\<^term>\<open>\<not> \<not> Suc x = 0\<close>), |
|
299 |
N (Cong, [N (Cong, [N (Let [\<^term>\<open>Suc x\<close>], [N (Refl, []), N (Refl, [])])])])); |
|
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
300 |
|
69597 | 301 |
reconstruct_proof \<^context> proof8 |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
302 |
\<close> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
303 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
304 |
ML \<open> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
305 |
val proof9 = |
69597 | 306 |
((\<^term>\<open>\<not> (let x = Suc x in x = 0)\<close>, |
307 |
\<^term>\<open>\<not> Suc x = 0\<close>), |
|
308 |
N (Cong, [N (Let [\<^term>\<open>Suc x\<close>], [N (Refl, []), N (Refl, [])])])); |
|
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
309 |
|
69597 | 310 |
reconstruct_proof \<^context> proof9 |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
311 |
\<close> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
312 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
313 |
ML \<open> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
314 |
val proof10 = |
69597 | 315 |
((\<^term>\<open>\<exists>x :: nat. p (x + 0)\<close>, |
316 |
\<^term>\<open>\<exists>x :: nat. p x\<close>), |
|
65017 | 317 |
N (Bind, [N (Cong, [N (Taut @{thm add_0_right}, [])])])); |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
318 |
|
69597 | 319 |
reconstruct_proof \<^context> proof10; |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
320 |
\<close> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
321 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
322 |
ML \<open> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
323 |
val proof11 = |
69597 | 324 |
((\<^term>\<open>\<not> (let (x, y) = (Suc y, Suc x) in y = 0)\<close>, |
325 |
\<^term>\<open>\<not> Suc x = 0\<close>), |
|
326 |
N (Cong, [N (Let [\<^term>\<open>Suc y\<close>, \<^term>\<open>Suc x\<close>], [N (Refl, []), N (Refl, []), |
|
65017 | 327 |
N (Refl, [])])])); |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
328 |
|
69597 | 329 |
reconstruct_proof \<^context> proof11 |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
330 |
\<close> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
331 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
332 |
ML \<open> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
333 |
val proof12 = |
69597 | 334 |
((\<^term>\<open>\<not> (let (x, y) = (Suc y, Suc x); (u, v, w) = (y, x, y) in w = 0)\<close>, |
335 |
\<^term>\<open>\<not> Suc x = 0\<close>), |
|
336 |
N (Cong, [N (Let [\<^term>\<open>Suc y\<close>, \<^term>\<open>Suc x\<close>], [N (Refl, []), N (Refl, []), |
|
337 |
N (Let [\<^term>\<open>Suc x\<close>, \<^term>\<open>Suc y\<close>, \<^term>\<open>Suc x\<close>], |
|
65017 | 338 |
[N (Refl, []), N (Refl, []), N (Refl, []), N (Refl, [])])])])); |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
339 |
|
69597 | 340 |
reconstruct_proof \<^context> proof12 |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
341 |
\<close> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
342 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
343 |
ML \<open> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
344 |
val proof13 = |
69597 | 345 |
((\<^term>\<open>\<not> \<not> (let x = Suc x in x = 0)\<close>, |
346 |
\<^term>\<open>\<not> \<not> Suc x = 0\<close>), |
|
347 |
N (Cong, [N (Cong, [N (Let [\<^term>\<open>Suc x\<close>], [N (Refl, []), N (Refl, [])])])])); |
|
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
348 |
|
69597 | 349 |
reconstruct_proof \<^context> proof13 |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
350 |
\<close> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
351 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
352 |
ML \<open> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
353 |
val proof14 = |
69597 | 354 |
((\<^term>\<open>let (x, y) = (f (a :: nat), b :: nat) in x > a\<close>, |
355 |
\<^term>\<open>f (a :: nat) > a\<close>), |
|
356 |
N (Let [\<^term>\<open>f (a :: nat) :: nat\<close>, \<^term>\<open>b :: nat\<close>], |
|
65017 | 357 |
[N (Cong, [N (Refl, [])]), N (Refl, []), N (Refl, [])])); |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
358 |
|
69597 | 359 |
reconstruct_proof \<^context> proof14 |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
360 |
\<close> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
361 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
362 |
ML \<open> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
363 |
val proof15 = |
69597 | 364 |
((\<^term>\<open>let x = (let y = g (z :: nat) in f (y :: nat)) in x = Suc 0\<close>, |
365 |
\<^term>\<open>f (g (z :: nat) :: nat) = Suc 0\<close>), |
|
366 |
N (Let [\<^term>\<open>f (g (z :: nat) :: nat) :: nat\<close>], |
|
367 |
[N (Let [\<^term>\<open>g (z :: nat) :: nat\<close>], [N (Refl, []), N (Refl, [])]), N (Refl, [])])); |
|
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
368 |
|
69597 | 369 |
reconstruct_proof \<^context> proof15 |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
370 |
\<close> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
371 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
372 |
ML \<open> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
373 |
val proof16 = |
69597 | 374 |
((\<^term>\<open>a > Suc b\<close>, |
375 |
\<^term>\<open>a > Suc b\<close>), |
|
376 |
N (Trans \<^term>\<open>a > Suc b\<close>, [N (Refl, []), N (Refl, [])])); |
|
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
377 |
|
69597 | 378 |
reconstruct_proof \<^context> proof16 |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
379 |
\<close> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
380 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
381 |
thm Suc_1 |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
382 |
thm numeral_2_eq_2 |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
383 |
thm One_nat_def |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
384 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
385 |
ML \<open> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
386 |
val proof17 = |
69597 | 387 |
((\<^term>\<open>2 :: nat\<close>, |
388 |
\<^term>\<open>Suc (Suc 0) :: nat\<close>), |
|
389 |
N (Trans \<^term>\<open>Suc 1\<close>, [N (Taut @{thm Suc_1[symmetric]}, []), N (Cong, |
|
65017 | 390 |
[N (Taut @{thm One_nat_def}, [])])])); |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
391 |
|
69597 | 392 |
reconstruct_proof \<^context> proof17 |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
393 |
\<close> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
394 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
395 |
ML \<open> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
396 |
val proof18 = |
69597 | 397 |
((\<^term>\<open>let x = a in let y = b in Suc x + y\<close>, |
398 |
\<^term>\<open>Suc a + b\<close>), |
|
399 |
N (Trans \<^term>\<open>let y = b in Suc a + y\<close>, |
|
400 |
[N (Let [\<^term>\<open>a :: nat\<close>], [N (Refl, []), N (Refl, [])]), |
|
401 |
N (Let [\<^term>\<open>b :: nat\<close>], [N (Refl, []), N (Refl, [])])])); |
|
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
402 |
|
69597 | 403 |
reconstruct_proof \<^context> proof18 |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
404 |
\<close> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
405 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
406 |
ML \<open> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
407 |
val proof19 = |
69597 | 408 |
((\<^term>\<open>\<forall>x. let x = f (x :: nat) :: nat in g x\<close>, |
409 |
\<^term>\<open>\<forall>x. g (f (x :: nat) :: nat)\<close>), |
|
410 |
N (Bind, [N (Let [\<^term>\<open>f :: nat \<Rightarrow> nat\<close> $ Bound 0], |
|
65017 | 411 |
[N (Refl, []), N (Refl, [])])])); |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
412 |
|
69597 | 413 |
reconstruct_proof \<^context> proof19 |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
414 |
\<close> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
415 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
416 |
ML \<open> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
417 |
val proof20 = |
69597 | 418 |
((\<^term>\<open>\<forall>x. let y = Suc 0 in let x = f (x :: nat) :: nat in g x\<close>, |
419 |
\<^term>\<open>\<forall>x. g (f (x :: nat) :: nat)\<close>), |
|
420 |
N (Bind, [N (Let [\<^term>\<open>Suc 0\<close>], [N (Refl, []), N (Let [\<^term>\<open>f (x :: nat) :: nat\<close>], |
|
65017 | 421 |
[N (Refl, []), N (Refl, [])])])])); |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
422 |
|
69597 | 423 |
reconstruct_proof \<^context> proof20 |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
424 |
\<close> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
425 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
426 |
ML \<open> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
427 |
val proof21 = |
69597 | 428 |
((\<^term>\<open>\<forall>x :: nat. let x = f x :: nat in let y = x in p y\<close>, |
429 |
\<^term>\<open>\<forall>z :: nat. p (f z :: nat)\<close>), |
|
430 |
N (Bind, [N (Let [\<^term>\<open>f (z :: nat) :: nat\<close>], |
|
431 |
[N (Refl, []), N (Let [\<^term>\<open>f (z :: nat) :: nat\<close>], |
|
65017 | 432 |
[N (Refl, []), N (Refl, [])])])])); |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
433 |
|
69597 | 434 |
reconstruct_proof \<^context> proof21 |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
435 |
\<close> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
436 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
437 |
ML \<open> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
438 |
val proof22 = |
69597 | 439 |
((\<^term>\<open>\<forall>x :: nat. let x = f x :: nat in let y = x in p y\<close>, |
440 |
\<^term>\<open>\<forall>x :: nat. p (f x :: nat)\<close>), |
|
441 |
N (Bind, [N (Let [\<^term>\<open>f (x :: nat) :: nat\<close>], |
|
442 |
[N (Refl, []), N (Let [\<^term>\<open>f (x :: nat) :: nat\<close>], |
|
65017 | 443 |
[N (Refl, []), N (Refl, [])])])])); |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
444 |
|
69597 | 445 |
reconstruct_proof \<^context> proof22 |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
446 |
\<close> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
447 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
448 |
ML \<open> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
449 |
val proof23 = |
69597 | 450 |
((\<^term>\<open>\<forall>x :: nat. let (x, a) = (f x :: nat, 0 ::nat) in let y = x in p y\<close>, |
451 |
\<^term>\<open>\<forall>z :: nat. p (f z :: nat)\<close>), |
|
452 |
N (Bind, [N (Let [\<^term>\<open>f (z :: nat) :: nat\<close>, \<^term>\<open>0 :: nat\<close>], |
|
453 |
[N (Refl, []), N (Refl, []), N (Let [\<^term>\<open>f (z :: nat) :: nat\<close>], |
|
65017 | 454 |
[N (Refl, []), N (Refl, [])])])])); |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
455 |
|
69597 | 456 |
reconstruct_proof \<^context> proof23 |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
457 |
\<close> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
458 |
|
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
459 |
ML \<open> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
460 |
val proof24 = |
69597 | 461 |
((\<^term>\<open>\<forall>x :: nat. let (x, a) = (f x :: nat, 0 ::nat) in let y = x in p y\<close>, |
462 |
\<^term>\<open>\<forall>x :: nat. p (f x :: nat)\<close>), |
|
463 |
N (Bind, [N (Let [\<^term>\<open>f (x :: nat) :: nat\<close>, \<^term>\<open>0 :: nat\<close>], |
|
464 |
[N (Refl, []), N (Refl, []), N (Let [\<^term>\<open>f (x :: nat) :: nat\<close>], |
|
65017 | 465 |
[N (Refl, []), N (Refl, [])])])])); |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
466 |
|
69597 | 467 |
reconstruct_proof \<^context> proof24 |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
468 |
\<close> |
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
469 |
|
69217 | 470 |
ML \<open> |
471 |
val proof25 = |
|
69597 | 472 |
((\<^term>\<open>let vr0 = vr1 in let vr1 = vr2 in vr0 + vr1 + vr2 :: nat\<close>, |
473 |
\<^term>\<open>vr1 + vr2 + vr2 :: nat\<close>), |
|
474 |
N (Trans \<^term>\<open>let vr1a = vr2 in vr1 + vr1a + vr2 :: nat\<close>, |
|
475 |
[N (Let [\<^term>\<open>vr1 :: nat\<close>], [N (Refl, []), N (Refl, [])]), |
|
476 |
N (Let [\<^term>\<open>vr2 :: nat\<close>], [N (Refl, []), N (Refl, [])])])); |
|
69217 | 477 |
|
69597 | 478 |
reconstruct_proof \<^context> proof25 |
69217 | 479 |
\<close> |
480 |
||
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset
|
481 |
end |