--- a/src/HOL/SMT_Examples/SMT_Examples_Verit.thy Fri Mar 11 14:02:13 2022 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples_Verit.thy Fri Mar 11 16:43:09 2022 +0100
@@ -649,32 +649,32 @@
fun_evaluate_match :: \<open>'astate \<Rightarrow> 'vsemv_env \<Rightarrow> _ \<Rightarrow> ('pat \<times> 'exp0) list \<Rightarrow> _ \<Rightarrow>
'astate*((('v)list),('v))result\<close>
assumes
- " fix_clock (st::'astate) (fun_evaluate st (env::'vsemv_env) [e::'exp0]) =
- (st'::'astate, r::('v list, 'v) result)"
- " clock (fst (fun_evaluate (st::'astate) (env::'vsemv_env) [e::'exp0])) \<le> clock st"
- "\<forall>(b::nat) (a::nat) c::nat. b \<le> a \<and> c \<le> b \<longrightarrow> c \<le> a"
- "\<forall>(a::'astate) p::'astate \<times> ('v list, 'v) result. (a = fst p) = (\<exists>b::('v list, 'v) result. p = (a, b))"
- "\<forall>y::'v error_result. (\<forall>x1::'v. y = Rraise x1 \<longrightarrow> False) \<and> (\<forall>x2::abort. y = Rabort x2 \<longrightarrow> False) \<longrightarrow> False"
- "\<forall>(f1::'v \<Rightarrow> 'astate \<times> ('v list, 'v) result) (f2::abort \<Rightarrow> 'astate \<times> ('v list, 'v) result) x1::'v.
- (case Rraise x1 of Rraise (x::'v) \<Rightarrow> f1 x | Rabort (x::abort) \<Rightarrow> f2 x) = f1 x1"
- " \<forall>(f1::'v \<Rightarrow> 'astate \<times> ('v list, 'v) result) (f2::abort \<Rightarrow> 'astate \<times> ('v list, 'v) result) x2::abort.
- (case Rabort x2 of Rraise (x::'v) \<Rightarrow> f1 x | Rabort (x::abort) \<Rightarrow> f2 x) = f2 x2"
- "\<forall>(s1::'astate) (s2::'astate) (x::('v list, 'v) result) s::'astate.
- fix_clock s1 (s2, x) = (s, x) \<longrightarrow> clock s \<le> clock s2"
- "\<forall>(s::'astate) (s'::'astate) res::('v list, 'v) result.
- fix_clock s (s', res) =
- (update_clock (\<lambda>_::nat. if clock s' \<le> clock s then clock s' else clock s) s', res)"
- "\<forall>(x2::'v error_result) x1::'v.
- (r::('v list, 'v) result) = Rerr x2 \<and> x2 = Rraise x1 \<longrightarrow>
- clock (fst (fun_evaluate_match (st'::'astate) (env::'vsemv_env) x1 (pes::('pat \<times> 'exp0) list) x1))
- \<le> clock st'"
- shows "((r::('v list, 'v) result) = Rerr (x2::'v error_result) \<longrightarrow>
+ "fix_clock (st::'astate) (fun_evaluate st (env::'vsemv_env) [e::'exp0]) =
+ (st'::'astate, r::('v list, 'v) result)"
+ "clock (fst (fun_evaluate (st::'astate) (env::'vsemv_env) [e::'exp0])) \<le> clock st"
+ "\<forall>(b::nat) (a::nat) c::nat. b \<le> a \<and> c \<le> b \<longrightarrow> c \<le> a"
+ "\<forall>(a::'astate) p::'astate \<times> ('v list, 'v) result. (a = fst p) = (\<exists>b::('v list, 'v) result. p = (a, b))"
+ "\<forall>y::'v error_result. (\<forall>x1::'v. y = Rraise x1 \<longrightarrow> False) \<and> (\<forall>x2::abort. y = Rabort x2 \<longrightarrow> False) \<longrightarrow> False"
+ "\<forall>(f1::'v \<Rightarrow> 'astate \<times> ('v list, 'v) result) (f2::abort \<Rightarrow> 'astate \<times> ('v list, 'v) result) x1::'v.
+ (case Rraise x1 of Rraise (x::'v) \<Rightarrow> f1 x | Rabort (x::abort) \<Rightarrow> f2 x) = f1 x1"
+ "\<forall>(f1::'v \<Rightarrow> 'astate \<times> ('v list, 'v) result) (f2::abort \<Rightarrow> 'astate \<times> ('v list, 'v) result) x2::abort.
+ (case Rabort x2 of Rraise (x::'v) \<Rightarrow> f1 x | Rabort (x::abort) \<Rightarrow> f2 x) = f2 x2"
+ "\<forall>(s1::'astate) (s2::'astate) (x::('v list, 'v) result) s::'astate.
+ fix_clock s1 (s2, x) = (s, x) \<longrightarrow> clock s \<le> clock s2"
+ "\<forall>(s::'astate) (s'::'astate) res::('v list, 'v) result.
+ fix_clock s (s', res) =
+ (update_clock (\<lambda>_::nat. if clock s' \<le> clock s then clock s' else clock s) s', res)"
+ "\<forall>(x2::'v error_result) x1::'v.
+ (r::('v list, 'v) result) = Rerr x2 \<and> x2 = Rraise x1 \<longrightarrow>
+ clock (fst (fun_evaluate_match (st'::'astate) (env::'vsemv_env) x1 (pes::('pat \<times> 'exp0) list) x1))
+ \<le> clock st'"
+ shows "((r::('v list, 'v) result) = Rerr (x2::'v error_result) \<longrightarrow>
clock
(fst (case x2 of
Rraise (v2::'v) \<Rightarrow>
fun_evaluate_match (st'::'astate) (env::'vsemv_env) v2 (pes::('pat \<times> 'exp0) list) v2
| Rabort (abort::abort) \<Rightarrow> (st', Rerr (Rabort abort))))
- \<le> clock (st::'astate)) "
+ \<le> clock (st::'astate))"
using assms by (smt (verit))
end
--- a/src/HOL/Tools/SMT/verit_replay_methods.ML Fri Mar 11 14:02:13 2022 +0100
+++ b/src/HOL/Tools/SMT/verit_replay_methods.ML Fri Mar 11 16:43:09 2022 +0100
@@ -901,6 +901,7 @@
f $ arg =>
(Conv.fun_conv (eq_pred_conv rews f ctxt) then_conv
Conv.arg_conv (eq_pred_conv rews arg ctxt)) ctrm
+ | Abs (_, _, f) => Conv.abs_conv (eq_pred_conv rews f o snd) ctxt ctrm
| _ => Conv.all_conv ctrm))
fun eq_pred_rewrite_tac ({context = ctxt, prems, concl, ...}: Subgoal.focus) =
@@ -917,6 +918,7 @@
| Const(_, _) $ t1 $ (Const(\<^const_name>\<open>HOL.Not\<close>, _) $ _) => (t1, conv_left_neg)
| Const(_, _) $ t1 $ _ => (t1, conv_left)
| t1 => (t1, conv_left))
+
fun throwing_CONVERSION cv i st = Seq.single (Conv.gconv_rule cv i st)
in
throwing_CONVERSION (conv_term (eq_pred_conv rews t1 ctxt))