Migration to Isabelle 2021-1 (based on afp-2021-12-28).
This commit is contained in:
parent
140ae6d623
commit
f1b3fa41c2
|
@ -1765,7 +1765,7 @@ proof -
|
||||||
"prefix (B@[\<langle>\<theta> x != \<theta> y\<rangle>]) (unlabel (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<theta>))) \<or>
|
"prefix (B@[\<langle>\<theta> x != \<theta> y\<rangle>]) (unlabel (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<theta>))) \<or>
|
||||||
prefix (B@[\<langle>\<theta> y != \<theta> x\<rangle>]) (unlabel (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<theta>)))"
|
prefix (B@[\<langle>\<theta> y != \<theta> x\<rangle>]) (unlabel (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<theta>)))"
|
||||||
unfolding prefix_def
|
unfolding prefix_def
|
||||||
by (metis (no_types, hide_lams) append.assoc append_Cons append_Nil split_list)
|
by (metis (no_types, opaque_lifting) append.assoc append_Cons append_Nil split_list)
|
||||||
thus ?thesis
|
thus ?thesis
|
||||||
using \<I> strand_sem_append_stateful[of IK DB _ _ \<I>]
|
using \<I> strand_sem_append_stateful[of IK DB _ _ \<I>]
|
||||||
stateful_strand_sem_NegChecks_no_bvars(2)
|
stateful_strand_sem_NegChecks_no_bvars(2)
|
||||||
|
@ -2550,7 +2550,7 @@ proof -
|
||||||
hence "\<exists>a. \<Gamma> (Var x) = TAtom a"
|
hence "\<exists>a. \<Gamma> (Var x) = TAtom a"
|
||||||
by simp
|
by simp
|
||||||
hence "\<exists>a. \<Gamma> (Fun f T) = TAtom a"
|
hence "\<exists>a. \<Gamma> (Fun f T) = TAtom a"
|
||||||
by (metis (no_types, hide_lams) \<I>' welltyped_constraint_model_def fT_p wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def)
|
by (metis (no_types, opaque_lifting) \<I>' welltyped_constraint_model_def fT_p wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def)
|
||||||
ultimately show "(\<exists>f. \<I> x = Fun f []) \<or> (\<exists>y. \<I> x = Var y)"
|
ultimately show "(\<exists>f. \<I> x = Fun f []) \<or> (\<exists>y. \<I> x = Var y)"
|
||||||
using TAtom_term_cases fT_p by metis
|
using TAtom_term_cases fT_p by metis
|
||||||
qed
|
qed
|
||||||
|
@ -3762,7 +3762,7 @@ proof (induction \<A> rule: reachable_constraints.induct)
|
||||||
by (metis IH n(1))
|
by (metis IH n(1))
|
||||||
thus ?thesis
|
thus ?thesis
|
||||||
using n x_nin_\<A> trms\<^sub>s\<^sub>s\<^sub>t_unlabel_prefix_subset(1)[of B]
|
using n x_nin_\<A> trms\<^sub>s\<^sub>s\<^sub>t_unlabel_prefix_subset(1)[of B]
|
||||||
by (metis (no_types, hide_lams) self_append_conv subset_iff subterms\<^sub>s\<^sub>e\<^sub>t_mono prefix_def)
|
by (metis (no_types, opaque_lifting) self_append_conv subset_iff subterms\<^sub>s\<^sub>e\<^sub>t_mono prefix_def)
|
||||||
qed (use n x_nin_\<A> in fastforce)
|
qed (use n x_nin_\<A> in fastforce)
|
||||||
qed
|
qed
|
||||||
|
|
||||||
|
|
|
@ -2296,7 +2296,7 @@ proof -
|
||||||
moreover
|
moreover
|
||||||
have "\<alpha> y = Var z"
|
have "\<alpha> y = Var z"
|
||||||
using zn
|
using zn
|
||||||
by (metis (no_types, hide_lams) \<sigma> subst_compose_def subst_imgI subst_to_var_is_var
|
by (metis (no_types, opaque_lifting) \<sigma> subst_compose_def subst_imgI subst_to_var_is_var
|
||||||
term.distinct(1) transaction_fresh_subst_def var_comp(2))
|
term.distinct(1) transaction_fresh_subst_def var_comp(2))
|
||||||
then have "\<alpha> y \<cdot> \<I> = \<I> z"
|
then have "\<alpha> y \<cdot> \<I> = \<I> z"
|
||||||
by auto
|
by auto
|
||||||
|
|
|
@ -620,7 +620,7 @@ proof -
|
||||||
|
|
||||||
have "take n S@drop n T = S1@T ! n#T2" "take (Suc n) S@drop (Suc n) T = S1@S ! n#T2"
|
have "take n S@drop n T = S1@T ! n#T2" "take (Suc n) S@drop (Suc n) T = S1@S ! n#T2"
|
||||||
using n T S append_eq_conv_conj
|
using n T S append_eq_conv_conj
|
||||||
by (metis, metis (no_types, hide_lams) Cons_nth_drop_Suc append.assoc append_Cons
|
by (metis, metis (no_types, opaque_lifting) Cons_nth_drop_Suc append.assoc append_Cons
|
||||||
append_Nil take_Suc_conv_app_nth)
|
append_Nil take_Suc_conv_app_nth)
|
||||||
moreover have "(T ! n, S ! n) \<in> timpl_closure' c" using IH Suc.prems by simp
|
moreover have "(T ! n, S ! n) \<in> timpl_closure' c" using IH Suc.prems by simp
|
||||||
ultimately show ?case
|
ultimately show ?case
|
||||||
|
|
|
@ -1,5 +1,6 @@
|
||||||
\documentclass[10pt,DIV16,a4paper,abstract=true,twoside=semi,openright]
|
\documentclass[10pt,DIV16,a4paper,abstract=true,twoside=semi,openright]
|
||||||
{scrreprt}
|
{scrreprt}
|
||||||
|
\usepackage[T1]{fontenc}
|
||||||
\usepackage[english]{babel}
|
\usepackage[english]{babel}
|
||||||
\usepackage[numbers, sort&compress]{natbib}
|
\usepackage[numbers, sort&compress]{natbib}
|
||||||
\usepackage{isabelle,isabellesym}
|
\usepackage{isabelle,isabellesym}
|
||||||
|
|
|
@ -279,7 +279,7 @@ structure ml_isar_wrapper = struct
|
||||||
|
|
||||||
fun prove_simple name stmt tactic lthy =
|
fun prove_simple name stmt tactic lthy =
|
||||||
let
|
let
|
||||||
val thm = Goal.prove lthy [] [] stmt (fn {context, ...} => tactic context)
|
val thm = Goal.prove lthy [] [] stmt (tactic o #context)
|
||||||
|> Goal.norm_result lthy
|
|> Goal.norm_result lthy
|
||||||
|> Goal.check_finished lthy
|
|> Goal.check_finished lthy
|
||||||
in
|
in
|
||||||
|
@ -1646,7 +1646,6 @@ structure trac = struct
|
||||||
(
|
(
|
||||||
type T = hide_tvar_tab
|
type T = hide_tvar_tab
|
||||||
val empty = Symtab.empty:hide_tvar_tab
|
val empty = Symtab.empty:hide_tvar_tab
|
||||||
val extend = I
|
|
||||||
fun merge(t1,t2) = merge_trac_tab (t1, t2)
|
fun merge(t1,t2) = merge_trac_tab (t1, t2)
|
||||||
);
|
);
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue