author  blanchet 
Thu, 01 Nov 2018 14:36:19 +0100  
changeset 69220  c6b15fc78f78 
parent 69217  a8c707352ccc 
child 69597  ff784d5a5bfb 
permissions  rwrr 
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 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

50 
(Const (@{const_name Let}, tuple_T > lambda_T > B) $ tuple_t $ lambda_t, q); 
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" 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

72 
 str_of_rule_name (Taut th) = "Taut[" ^ @{make_string} th ^ "]" 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

73 
 str_of_rule_name (Trans t) = "Trans[" ^ Syntax.string_of_term @{context} t ^ "]" 
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) = 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

79 
"Let[" ^ commas (map (Syntax.string_of_term @{context}) ts) ^ "]"; 
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 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

85 
 lambda_count ((t as Const (@{const_name case_prod}, _) $ _) $ _) = lambda_count t  1 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

86 
 lambda_count (Const (@{const_name case_prod}, _) $ t) = lambda_count t  1 
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 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

99 
 zo 0 bound_Ts ((t as Const (@{const_name case_prod}, _) $ _) $ arg, u) = 
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 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

104 
 zo n bound_Ts (Const (@{const_name case_prod}, 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

105 
Type (@{type_name fun}, [Type (@{type_name fun}, [A, Type (@{type_name fun}, [B, _])]), 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

106 
Type (@{type_name fun}, [AB, _])])) $ t, u) = 
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 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

111 
(Const (@{const_name case_prod}, (A > B > C) > AB > C) $ t', u') 
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 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

133 
(Const (@{const_name All}, _) $ Abs (_, T, t), Const (@{const_name All}, _) $ Abs (s, U, u)) => 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

134 
(Abs (s, T, t), Abs (s, U, u)) 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

135 
 (Const (@{const_name Ex}, _) $ t, Const (@{const_name Ex}, _) $ u) => (t, u) 
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 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

140 
Const (@{const_name Ex}, _) $ (t as Abs (_, T, _)) => 
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 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

146 
Const (@{const_name All}, _) $ (t as Abs (s, T, body)) => 
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 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

152 
Const (@{const_name Let}, _) $ t $ _ => 
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 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

161 
Const (@{const_name Let}, _) $ _ $ u => (u $ t', rhs) 
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 

5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

170 
val _ = warning (Syntax.string_of_term @{context} goal); 
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 = 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

222 
((@{term "\<exists>x :: nat. p x"}, 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

223 
@{term "p (SOME x :: nat. p x)"}), 
65017  224 
N (Sko_Ex, [N (Refl, [])])); 
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

225 

5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

226 
reconstruct_proof @{context} proof0; 
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 = 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

231 
((@{term "\<not> (\<forall>x :: nat. \<exists>y :: nat. p x y)"}, 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

232 
@{term "\<not> (\<exists>y :: nat. p (SOME x :: nat. \<not> (\<exists>y :: nat. p x y)) y)"}), 
65017  233 
N (Cong, [N (Sko_All, [N (Bind, [N (Refl, [])])])])); 
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

234 

5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

235 
reconstruct_proof @{context} proof1; 
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 = 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

240 
((@{term "\<forall>x :: nat. \<exists>y :: nat. \<exists>z :: nat. p x y z"}, 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

241 
@{term "\<forall>x :: nat. p x (SOME y :: nat. \<exists>z :: nat. p x y z) 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

242 
(SOME z :: nat. p x (SOME y :: nat. \<exists>z :: nat. p x y z) z)"}), 
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 

5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

245 
reconstruct_proof @{context} proof2 
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 = 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

250 
((@{term "\<forall>x :: nat. \<exists>x :: nat. \<exists>x :: nat. p x x x"}, 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

251 
@{term "\<forall>x :: nat. p (SOME x :: nat. p x x x) (SOME x. p x x x) (SOME x. p x x x)"}), 
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 

5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

254 
reconstruct_proof @{context} proof3 
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 = 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

259 
((@{term "\<forall>x :: nat. \<exists>x :: nat. \<exists>x :: nat. p x x x"}, 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

260 
@{term "\<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)"}), 
65017  261 
N (Bind, [N (Bind, [N (Sko_Ex, [N (Refl, [])])])])); 
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

262 

5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

263 
reconstruct_proof @{context} proof4 
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 = 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

268 
((@{term "\<forall>x :: nat. q \<and> (\<exists>x :: nat. \<exists>x :: nat. p x x x)"}, 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

269 
@{term "\<forall>x :: nat. q \<and> 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

270 
(\<exists>x :: nat. p (SOME x :: nat. p x x x) (SOME x. p x x x) (SOME x. p x x x))"}), 
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 

5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

273 
reconstruct_proof @{context} proof5 
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 = 
65016  278 
((@{term "\<not> (\<forall>x :: nat. p \<and> (\<exists>x :: nat. \<forall>x :: nat. q x x))"}, 
279 
@{term "\<not> (\<forall>x :: nat. p \<and> 

280 
(\<exists>x :: nat. q (SOME x :: nat. \<not> q x x) (SOME x. \<not> q x x)))"}), 

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 

5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

283 
reconstruct_proof @{context} proof6 
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 = 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

288 
((@{term "\<not> \<not> (\<exists>x. p x)"}, 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

289 
@{term "\<not> \<not> p (SOME x. p x)"}), 
65017  290 
N (Cong, [N (Cong, [N (Sko_Ex, [N (Refl, [])])])])); 
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

291 

5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

292 
reconstruct_proof @{context} proof7 
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 = 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

297 
((@{term "\<not> \<not> (let x = Suc x in x = 0)"}, 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

298 
@{term "\<not> \<not> Suc x = 0"}), 
65017  299 
N (Cong, [N (Cong, [N (Let [@{term "Suc x"}], [N (Refl, []), N (Refl, [])])])])); 
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

300 

5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

301 
reconstruct_proof @{context} proof8 
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 = 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

306 
((@{term "\<not> (let x = Suc x in x = 0)"}, 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

307 
@{term "\<not> Suc x = 0"}), 
65017  308 
N (Cong, [N (Let [@{term "Suc x"}], [N (Refl, []), N (Refl, [])])])); 
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

309 

5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

310 
reconstruct_proof @{context} proof9 
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 = 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

315 
((@{term "\<exists>x :: nat. p (x + 0)"}, 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

316 
@{term "\<exists>x :: nat. p x"}), 
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 

5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

319 
reconstruct_proof @{context} proof10; 
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 = 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

324 
((@{term "\<not> (let (x, y) = (Suc y, Suc x) in y = 0)"}, 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

325 
@{term "\<not> Suc x = 0"}), 
65017  326 
N (Cong, [N (Let [@{term "Suc y"}, @{term "Suc x"}], [N (Refl, []), N (Refl, []), 
327 
N (Refl, [])])])); 

64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

328 

5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

329 
reconstruct_proof @{context} proof11 
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 = 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

334 
((@{term "\<not> (let (x, y) = (Suc y, Suc x); (u, v, w) = (y, x, y) in w = 0)"}, 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

335 
@{term "\<not> Suc x = 0"}), 
65017  336 
N (Cong, [N (Let [@{term "Suc y"}, @{term "Suc x"}], [N (Refl, []), N (Refl, []), 
337 
N (Let [@{term "Suc x"}, @{term "Suc y"}, @{term "Suc x"}], 

338 
[N (Refl, []), N (Refl, []), N (Refl, []), N (Refl, [])])])])); 

64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

339 

5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

340 
reconstruct_proof @{context} proof12 
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 = 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

345 
((@{term "\<not> \<not> (let x = Suc x in x = 0)"}, 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

346 
@{term "\<not> \<not> Suc x = 0"}), 
65017  347 
N (Cong, [N (Cong, [N (Let [@{term "Suc x"}], [N (Refl, []), N (Refl, [])])])])); 
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

348 

5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

349 
reconstruct_proof @{context} proof13 
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 = 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

354 
((@{term "let (x, y) = (f (a :: nat), b :: nat) in x > a"}, 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

355 
@{term "f (a :: nat) > a"}), 
65017  356 
N (Let [@{term "f (a :: nat) :: nat"}, @{term "b :: nat"}], 
357 
[N (Cong, [N (Refl, [])]), N (Refl, []), N (Refl, [])])); 

64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

358 

5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

359 
reconstruct_proof @{context} proof14 
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 = 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

364 
((@{term "let x = (let y = g (z :: nat) in f (y :: nat)) in x = Suc 0"}, 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

365 
@{term "f (g (z :: nat) :: nat) = Suc 0"}), 
65017  366 
N (Let [@{term "f (g (z :: nat) :: nat) :: nat"}], 
367 
[N (Let [@{term "g (z :: nat) :: nat"}], [N (Refl, []), N (Refl, [])]), N (Refl, [])])); 

64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

368 

5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

369 
reconstruct_proof @{context} proof15 
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 = 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

374 
((@{term "a > Suc b"}, 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

375 
@{term "a > Suc b"}), 
65017  376 
N (Trans @{term "a > Suc b"}, [N (Refl, []), N (Refl, [])])); 
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

377 

5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

378 
reconstruct_proof @{context} proof16 
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 = 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

387 
((@{term "2 :: nat"}, 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

388 
@{term "Suc (Suc 0) :: nat"}), 
65017  389 
N (Trans @{term "Suc 1"}, [N (Taut @{thm Suc_1[symmetric]}, []), N (Cong, 
390 
[N (Taut @{thm One_nat_def}, [])])])); 

64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

391 

5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

392 
reconstruct_proof @{context} proof17 
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 = 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

397 
((@{term "let x = a in let y = b in Suc x + y"}, 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

398 
@{term "Suc a + b"}), 
65017  399 
N (Trans @{term "let y = b in Suc a + y"}, 
400 
[N (Let [@{term "a :: nat"}], [N (Refl, []), N (Refl, [])]), 

401 
N (Let [@{term "b :: nat"}], [N (Refl, []), N (Refl, [])])])); 

64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

402 

5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

403 
reconstruct_proof @{context} proof18 
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 = 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

408 
((@{term "\<forall>x. let x = f (x :: nat) :: nat in g x"}, 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

409 
@{term "\<forall>x. g (f (x :: nat) :: nat)"}), 
65017  410 
N (Bind, [N (Let [@{term "f :: nat \<Rightarrow> nat"} $ Bound 0], 
411 
[N (Refl, []), N (Refl, [])])])); 

64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

412 

5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

413 
reconstruct_proof @{context} proof19 
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 = 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

418 
((@{term "\<forall>x. let y = Suc 0 in let x = f (x :: nat) :: nat in g x"}, 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

419 
@{term "\<forall>x. g (f (x :: nat) :: nat)"}), 
65017  420 
N (Bind, [N (Let [@{term "Suc 0"}], [N (Refl, []), N (Let [@{term "f (x :: nat) :: nat"}], 
421 
[N (Refl, []), N (Refl, [])])])])); 

64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

422 

5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

423 
reconstruct_proof @{context} proof20 
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 = 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

428 
((@{term "\<forall>x :: nat. let x = f x :: nat in let y = x in p y"}, 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

429 
@{term "\<forall>z :: nat. p (f z :: nat)"}), 
65017  430 
N (Bind, [N (Let [@{term "f (z :: nat) :: nat"}], 
431 
[N (Refl, []), N (Let [@{term "f (z :: nat) :: nat"}], 

432 
[N (Refl, []), N (Refl, [])])])])); 

64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

433 

5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

434 
reconstruct_proof @{context} proof21 
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 = 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

439 
((@{term "\<forall>x :: nat. let x = f x :: nat in let y = x in p y"}, 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

440 
@{term "\<forall>x :: nat. p (f x :: nat)"}), 
65017  441 
N (Bind, [N (Let [@{term "f (x :: nat) :: nat"}], 
442 
[N (Refl, []), N (Let [@{term "f (x :: nat) :: nat"}], 

443 
[N (Refl, []), N (Refl, [])])])])); 

64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

444 

5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

445 
reconstruct_proof @{context} proof22 
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 = 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

450 
((@{term "\<forall>x :: nat. let (x, a) = (f x :: nat, 0 ::nat) in let y = x in p y"}, 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

451 
@{term "\<forall>z :: nat. p (f z :: nat)"}), 
65017  452 
N (Bind, [N (Let [@{term "f (z :: nat) :: nat"}, @{term "0 :: nat"}], 
453 
[N (Refl, []), N (Refl, []), N (Let [@{term "f (z :: nat) :: nat"}], 

454 
[N (Refl, []), N (Refl, [])])])])); 

64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

455 

5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

456 
reconstruct_proof @{context} proof23 
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 = 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

461 
((@{term "\<forall>x :: nat. let (x, a) = (f x :: nat, 0 ::nat) in let y = x in p y"}, 
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

462 
@{term "\<forall>x :: nat. p (f x :: nat)"}), 
65017  463 
N (Bind, [N (Let [@{term "f (x :: nat) :: nat"}, @{term "0 :: nat"}], 
464 
[N (Refl, []), N (Refl, []), N (Let [@{term "f (x :: nat) :: nat"}], 

465 
[N (Refl, []), N (Refl, [])])])])); 

64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

466 

5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

467 
reconstruct_proof @{context} proof24 
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 = 

472 
((@{term "let vr0 = vr1 in let vr1 = vr2 in vr0 + vr1 + vr2 :: nat"}, 

473 
@{term "vr1 + vr2 + vr2 :: nat"}), 

474 
N (Trans @{term "let vr1a = vr2 in vr1 + vr1a + vr2 :: nat"}, 

475 
[N (Let [@{term "vr1 :: nat"}], [N (Refl, []), N (Refl, [])]), 

476 
N (Let [@{term "vr2 :: nat"}], [N (Refl, []), N (Refl, [])])])); 

477 

69220  478 
reconstruct_proof @{context} proof25 
69217  479 
\<close> 
480 

64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
diff
changeset

481 
end 