From cdf11e47ca07cd262f517e863babdd154c179ca8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Tuong?=
<tuong@users.noreply.github.com>
Date: Sun, 26 Dec 2021 22:16:40 -0800
Subject: [PATCH] upgrade to Isabelle2021-1
---
.../archive/uml_ocl/Isabelle_Finite_Set.thy | 2 +-
.../uml_ocl/OCL_lib_Gogolla_challenge.thy | 45 +++++++-----
.../OCL_lib_Gogolla_challenge_naive.thy | 26 ++++---
Citadelle/src/collection_types/UML_Bag.thy | 52 +++++++-------
Citadelle/src/collection_types/UML_Set.thy | 68 ++++++++++---------
.../compiler/Generator_dynamic_sequential.thy | 58 +++++++++-------
.../Generator_dynamic_concurrent.thy | 58 +++++++++-------
.../Generator_dynamic_export_testing.thy | 47 ++++++++-----
.../meta_isabelle/Meta_Isabelle.thy | 2 +-
.../Generator_dynamic_sequential.thy | 36 ++++++----
Citadelle/src/compiler_misc/Aux_text.thy | 1 -
.../src/compiler_misc/meta/Printer_init.thy | 1 -
.../src/uml_main/UML_PropertyProfiles.thy | 4 +-
Citadelle/src/uml_main/UML_State.thy | 16 ++---
14 files changed, 238 insertions(+), 178 deletions(-)
diff --git a/Citadelle/examples/archive/uml_ocl/Isabelle_Finite_Set.thy b/Citadelle/examples/archive/uml_ocl/Isabelle_Finite_Set.thy
index 224ea0a3622..5d21c80393e 100644
--- a/Citadelle/examples/archive/uml_ocl/Isabelle_Finite_Set.thy
+++ b/Citadelle/examples/archive/uml_ocl/Isabelle_Finite_Set.thy
@@ -82,7 +82,7 @@ term "all_defined \<tau> (f \<zero> Set{\<zero>}) = (all_defined \<tau> Set{\<ze
lemma int_trivial : "is_int (\<lambda>_. \<lfloor>a\<rfloor>)" by(simp add: is_int_def OclValid_def valid_def bot_fun_def bot_option_def)
lemma EQ_sym : "(x::(_, _) Set) = y \<Longrightarrow> \<tau> \<Turnstile> \<upsilon> x \<Longrightarrow> \<tau> \<Turnstile> (x \<doteq> y)"
-by (metis (hide_lams, no_types) OclIf_true' OclValid_def StrictRefEq\<^sub>S\<^sub>e\<^sub>t.refl_ext)
+by (metis (opaque_lifting, no_types) OclIf_true' OclValid_def StrictRefEq\<^sub>S\<^sub>e\<^sub>t.refl_ext)
lemma cp_all_def : "all_defined \<tau> f = all_defined \<tau>' (\<lambda>_. f \<tau>)"
apply(simp add: all_defined_def all_defined_set'_def OclValid_def)
diff --git a/Citadelle/examples/archive/uml_ocl/OCL_lib_Gogolla_challenge.thy b/Citadelle/examples/archive/uml_ocl/OCL_lib_Gogolla_challenge.thy
index 17fdb9ca73a..a9f3d4194f4 100644
--- a/Citadelle/examples/archive/uml_ocl/OCL_lib_Gogolla_challenge.thy
+++ b/Citadelle/examples/archive/uml_ocl/OCL_lib_Gogolla_challenge.thy
@@ -117,7 +117,7 @@ proof -
qed
lemma cp_mtSet : "\<And>x. Set{} = (\<lambda>_. Set{} x)"
-by (metis (hide_lams, no_types) mtSet_def)
+by (metis (opaque_lifting, no_types) mtSet_def)
section{* Properties: OclIncluding *}
@@ -160,7 +160,7 @@ lemmas including_subst_set' = OclIncluding_cong'
lemma including_subst_set'' : "\<tau> \<Turnstile> \<delta> s \<Longrightarrow> \<tau> \<Turnstile> \<delta> t \<Longrightarrow> \<tau> \<Turnstile> \<upsilon> x \<Longrightarrow> (s::('\<AA>,'a::null)Set) \<tau> = t \<tau> \<Longrightarrow> s->including\<^sub>S\<^sub>e\<^sub>t(x) \<tau> = (t->including\<^sub>S\<^sub>e\<^sub>t(x)) \<tau>"
apply(frule including_subst_set'[where s = s and t = t and x = x], simp_all del: StrictRefEq\<^sub>S\<^sub>e\<^sub>t_exec)
apply(simp add: StrictRefEq\<^sub>S\<^sub>e\<^sub>t OclValid_def del: StrictRefEq\<^sub>S\<^sub>e\<^sub>t_exec)
- apply (metis (hide_lams, no_types) OclValid_def foundation20 foundation22)
+ apply (metis (opaque_lifting, no_types) OclValid_def foundation20 foundation22)
by (metis UML_Set.OclIncluding.cp0)
@@ -542,11 +542,17 @@ lemma if_commute_gen_var_gen :
and comm : "\<And>x y S \<tau>. F y (f x S) \<tau> = f x (F y S) \<tau>"
shows "comp_fun_commute (\<lambda>j r2. if c j then (F j r2) else f j r2 endif)"
proof -
+ interpret f_comm: comp_fun_commute f
+ by (fact f_comm)
+
+ interpret F_comm: comp_fun_commute F
+ by (fact F_comm)
+
have F_comm : "\<And>y x S. (F y (F x S)) = (F x (F y S))"
- by (metis comp_fun_commute.fun_left_comm F_comm)
+ by (simp add: F_comm.fun_left_comm)
have f_comm : "\<And>y x S. (f y (f x S)) = (f x (f y S))"
- by (metis comp_fun_commute.fun_left_comm f_comm)
+ by (simp add: f_comm.fun_left_comm)
have if_id : "\<And>x. (if x then invalid else invalid endif) = invalid"
by(rule ext,simp add: OclIf_def)
@@ -581,8 +587,11 @@ lemma including_commute_gen_var_gen :
and f_out : "\<And>x y S \<tau>. F x (S->including\<^sub>S\<^sub>e\<^sub>t(y)) \<tau> = (F x S)->including\<^sub>S\<^sub>e\<^sub>t(y) \<tau>"
shows "comp_fun_commute (\<lambda>j r2. ((F j r2)->including\<^sub>S\<^sub>e\<^sub>t(a)))"
proof -
+ interpret f_comm: comp_fun_commute F
+ by (fact f_comm)
+
have comm : "\<And>y x S. (F y (F x S)) = (F x (F y S))"
- by (metis comp_fun_commute.fun_left_comm f_comm)
+ by (simp add: f_comm.fun_left_comm)
show ?thesis
apply(simp add: comp_fun_commute_def comp_def)
apply(rule allI)+
@@ -761,16 +770,16 @@ proof -
apply(rule conjI, rule conjI) apply(subst (1 2) UML_Set.OclIncluding.cp0, simp)
apply(rule conjI) apply(subst (1 2) UML_Set.OclIncluding.cp0, subst (1 3) UML_Set.OclIncluding.cp0, subst (1 4) UML_Set.OclIncluding.cp0, simp) apply(rule allI)+
apply(rule impI)+
- apply(rule including_cp_all) apply(simp) apply (metis (hide_lams, no_types) all_defined1 cons_all_def i_val j_val)
- apply(rule including_cp_all) apply(simp) apply(simp add: j_int) apply (metis (hide_lams, no_types) all_defined1 cons_all_def i_val)
+ apply(rule including_cp_all) apply(simp) apply (metis (opaque_lifting, no_types) all_defined1 cons_all_def i_val j_val)
+ apply(rule including_cp_all) apply(simp) apply(simp add: j_int) apply (metis (opaque_lifting, no_types) all_defined1 cons_all_def i_val)
apply(rule including_cp_all) apply(simp) apply(simp add: i_int) apply(rule all_defined1, blast) apply(simp)
apply(rule conjI) apply(rule allI)+
apply(rule impI)+
- apply(rule including_notempty) apply (metis (hide_lams, no_types) all_defined1 cons_all_def i_val j_val) apply(simp)
- apply(rule including_notempty) apply (metis (hide_lams, no_types) all_defined1 cons_all_def i_val) apply(simp add: j_val)
+ apply(rule including_notempty) apply (metis (opaque_lifting, no_types) all_defined1 cons_all_def i_val j_val) apply(simp)
+ apply(rule including_notempty) apply (metis (opaque_lifting, no_types) all_defined1 cons_all_def i_val) apply(simp add: j_val)
apply(rule including_notempty) apply(rule all_defined1, blast) apply(simp add: i_val) apply(simp)
- by (metis (no_types, hide_lams) OclIncluding_commute cons_all_def' i_val invert_all_defined j_val)
+ by (metis (no_types, opaque_lifting) OclIncluding_commute cons_all_def' i_val invert_all_defined j_val)
qed
section{* Properties: (with comp fun commute) OclIterate *}
@@ -1334,7 +1343,7 @@ lemma iterate_commute' :
apply(drule_tac f = "\<lambda>s. Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e \<lfloor>\<lfloor>s\<rfloor>\<rfloor>" in arg_cong)
apply(subgoal_tac "S \<tau> = Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e \<lfloor>\<lfloor>{}\<rfloor>\<rfloor>")
prefer 2
- apply(metis (hide_lams, no_types) abs_rep_simp' all_defined_def)
+ apply(metis (opaque_lifting, no_types) abs_rep_simp' all_defined_def)
apply(simp add: mtSet_def)
apply(subst (1 2) cp_OclIterate1[OF f_comm]) apply(rule i_cons_all_def'[OF f_comm], blast)+
@@ -1472,7 +1481,7 @@ proof -
apply(drule_tac x = \<tau> in allE) prefer 2 apply assumption
apply(drule_tac x = \<tau> in allE) prefer 2 apply assumption
apply(simp add: mtSet_def)
- by (metis (hide_lams, no_types) abs_rep_simp' all_defined_def)
+ by (metis (opaque_lifting, no_types) abs_rep_simp' all_defined_def)
have invert_set_0 : "\<And>x F. \<lfloor>\<lfloor>insert x F\<rfloor>\<rfloor> \<in> {X. X = bot \<or> X = null \<or> (\<forall>x\<in>\<lceil>\<lceil>X\<rceil>\<rceil>. x \<noteq> bot)} \<Longrightarrow> \<lfloor>\<lfloor>F\<rfloor>\<rfloor> \<in> {X. X = bot \<or> X = null \<or> (\<forall>x\<in>\<lceil>\<lceil>X\<rceil>\<rceil>. x \<noteq> bot)}"
by(auto simp: bot_option_def null_option_def)
@@ -1677,7 +1686,7 @@ proof -
apply(drule_tac f = "\<lambda>s. Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e \<lfloor>\<lfloor>s\<rfloor>\<rfloor>" in arg_cong)
apply(subgoal_tac "S \<tau> = Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e \<lfloor>\<lfloor>{}\<rfloor>\<rfloor>")
prefer 2
- apply(metis (hide_lams, no_types) abs_rep_simp' all_defined_def)
+ apply(metis (opaque_lifting, no_types) abs_rep_simp' all_defined_def)
apply(simp add: mtSet_def)
apply(subst (1 2) UML_Set.OclIncluding.cp0)
@@ -1746,7 +1755,7 @@ proof -
apply(drule_tac f = "\<lambda>s. Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e \<lfloor>\<lfloor>s\<rfloor>\<rfloor>" in arg_cong)
apply(subgoal_tac "S \<tau> = Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e \<lfloor>\<lfloor>{}\<rfloor>\<rfloor>")
prefer 2
- apply (metis (hide_lams, no_types) abs_rep_simp' all_defined_def prod.exhaust)
+ apply (metis (opaque_lifting, no_types) abs_rep_simp' all_defined_def prod.exhaust)
apply(simp add: mtSet_def)
@@ -2846,6 +2855,10 @@ lemma select_iterate:
and P_strict: "\<And>x. x \<tau> = \<bottom> \<Longrightarrow> (P x) \<tau> = \<bottom>"
shows "UML_Set.OclSelect S P \<tau> = (S->iterate\<^sub>S\<^sub>e\<^sub>t(x; acc = Set{} | OclSelect_body P x acc)) \<tau>"
proof -
+ interpret OclSelect_body_commute: comp_fun_commute "(OclSelect_body (P::(('\<AA> state \<times> '\<AA> state \<Rightarrow> 'a option option)
+ \<Rightarrow> '\<AA> state \<times> '\<AA> state \<Rightarrow> bool option option)))"
+ by (fact OclSelect_body_commute)
+
have ex_insert : "\<And>x F P. (\<exists>x\<in>insert x F. P x) = (P x \<or> (\<exists>x\<in>F. P x))"
by (metis insert_iff)
@@ -2866,7 +2879,7 @@ proof -
by (case_tac " P \<tau> = \<bottom> \<or> P \<tau> = null", simp_all add: true_def)
have not_strongeq : "\<And>P. P \<tau> \<noteq> invalid \<tau> \<Longrightarrow> \<not> \<tau> \<Turnstile> P \<doteq> false \<Longrightarrow> (P \<doteq> false) \<tau> = false \<tau>"
- by (metis (hide_lams, no_types) OclValid_def StrictRefEq\<^sub>B\<^sub>o\<^sub>o\<^sub>l\<^sub>e\<^sub>a\<^sub>n.defined_args_valid bool_split_0 foundation1 foundation16 foundation18 invalid_def null_fun_def valid4)
+ by (metis (opaque_lifting, no_types) OclValid_def StrictRefEq\<^sub>B\<^sub>o\<^sub>o\<^sub>l\<^sub>e\<^sub>a\<^sub>n.defined_args_valid bool_split_0 foundation1 foundation16 foundation18 invalid_def null_fun_def valid4)
show ?thesis
@@ -2885,7 +2898,7 @@ proof -
apply(simp add: mtSet_def)
(* *)
apply(simp only: image_insert)
- apply(subst comp_fun_commute.fold_insert[OF OclSelect_body_commute], simp)
+ apply(subst OclSelect_body_commute.fold_insert, simp)
apply(rule inj, fast)
apply(simp only: OclSelect_body_def)
diff --git a/Citadelle/examples/archive/uml_ocl/OCL_lib_Gogolla_challenge_naive.thy b/Citadelle/examples/archive/uml_ocl/OCL_lib_Gogolla_challenge_naive.thy
index ad3ef3d0427..c2fb0b610e5 100644
--- a/Citadelle/examples/archive/uml_ocl/OCL_lib_Gogolla_challenge_naive.thy
+++ b/Citadelle/examples/archive/uml_ocl/OCL_lib_Gogolla_challenge_naive.thy
@@ -62,6 +62,8 @@ and F_commute: "comp_fun_commute F"
and F_valid_arg: "\<And>a A. \<upsilon> (F a A) = (\<upsilon> a and \<upsilon> A)"
shows "\<upsilon> (S->iterate\<^sub>S\<^sub>e\<^sub>t(a; x = A | F a x)) = (\<delta> S and (S->forAll\<^sub>S\<^sub>e\<^sub>t(x | \<upsilon> x)) and \<upsilon> A)"
proof -
+ interpret F_commute: comp_fun_commute F
+ by (fact F_commute)
have defined_inject_true : "\<And>\<tau> P. (\<delta> P) \<tau> \<noteq> true \<tau> \<Longrightarrow> (\<delta> P) \<tau> = false \<tau>"
apply(simp add: defined_def true_def false_def
@@ -128,8 +130,7 @@ proof -
apply(subgoal_tac "F (\<lambda>\<tau>. xa) (Finite_Set.fold F A ((\<lambda>a \<tau>. a) ` Fa)) = F (\<lambda>\<tau>. xa) xb")
prefer 2
apply(simp)
- apply(subst comp_fun_commute.fold_insert[where f = F and z = A and A = "((\<lambda>a \<tau>. a) ` Fa)" and x = "(\<lambda>\<tau>. xa)"])
- apply(rule F_commute)
+ apply(subst F_commute.fold_insert[where z = A and A = "((\<lambda>a \<tau>. a) ` Fa)" and x = "(\<lambda>\<tau>. xa)"])
apply(simp)
apply(rule image_cong)
apply(rule inject)
@@ -169,8 +170,7 @@ proof -
apply(subgoal_tac "\<forall>x. Finite_Set.fold F A (insert (\<lambda>\<tau>. xa) ((\<lambda>a \<tau>. a) ` Fa)) = x \<longrightarrow> (\<upsilon> x) \<tau> = false \<tau>") apply(simp, rule allI, rule impI)
apply(subgoal_tac "F (\<lambda>\<tau>. xa) (Finite_Set.fold F A ((\<lambda>a \<tau>. a) ` Fa)) = xc")
prefer 2
- apply(subst comp_fun_commute.fold_insert[where f = F and z = A and x = "(\<lambda>\<tau>. xa)" and A = "((\<lambda>a \<tau>. a) ` Fa)", symmetric])
- apply(rule F_commute)
+ apply(subst F_commute.fold_insert[where z = A and x = "(\<lambda>\<tau>. xa)" and A = "((\<lambda>a \<tau>. a) ` Fa)", symmetric])
apply(simp)
apply(rule image_cong)
apply(rule inject)
@@ -191,8 +191,7 @@ proof -
apply(subgoal_tac "F (\<lambda>\<tau>. xa) (Finite_Set.fold F A ((\<lambda>a \<tau>. a) ` Fa)) = F (\<lambda>\<tau>. xa) xd")
prefer 2
apply(simp)
- apply(subst comp_fun_commute.fold_insert[where f = F and z = A and A = "((\<lambda>a \<tau>. a) ` Fa)" and x = "(\<lambda>\<tau>. xa)"])
- apply(rule F_commute)
+ apply(subst F_commute.fold_insert[where z = A and A = "((\<lambda>a \<tau>. a) ` Fa)" and x = "(\<lambda>\<tau>. xa)"])
apply(simp)
apply(rule image_cong)
apply(rule inject)
@@ -275,6 +274,9 @@ and F_valid_arg_false2: "\<And>\<tau> a A. \<not> (\<tau> \<Turnstile> \<upsilon
shows "\<upsilon> (S->iterate\<^sub>S\<^sub>e\<^sub>t(a; x = A | F a x)) = (\<delta> S and (S->forAll\<^sub>S\<^sub>e\<^sub>t(x | \<upsilon> x)) and \<upsilon> A)"
proof -
+ interpret F_commute: comp_fun_commute F
+ by (fact F_commute)
+
have defined_inject_true : "\<And>\<tau> P. (\<delta> P) \<tau> \<noteq> true \<tau> \<Longrightarrow> (\<delta> P) \<tau> = false \<tau>"
apply(simp add: defined_def true_def false_def
bot_fun_def bot_option_def
@@ -334,8 +336,7 @@ proof -
apply(subgoal_tac "F (\<lambda>\<tau>. xa) (Finite_Set.fold F A ((\<lambda>a \<tau>. a) ` Fa)) = F (\<lambda>\<tau>. xa) xb")
prefer 2
apply(simp)
- apply(subst comp_fun_commute.fold_insert[where f = F and z = A and A = "((\<lambda>a \<tau>. a) ` Fa)" and x = "(\<lambda>\<tau>. xa)"])
- apply(rule F_commute)
+ apply(subst F_commute.fold_insert[where z = A and A = "((\<lambda>a \<tau>. a) ` Fa)" and x = "(\<lambda>\<tau>. xa)"])
apply(simp)
apply(rule image_cong)
apply(rule inject)
@@ -354,8 +355,7 @@ proof -
apply(insert A_defined, simp)
defer
apply(simp)
- apply(subst comp_fun_commute.fold_insert)
- apply(rule F_commute)
+ apply(subst F_commute.fold_insert)
apply(simp)
apply(simp)
apply(simp add: Let_def)
@@ -387,8 +387,7 @@ proof -
apply(subgoal_tac "\<forall>x. Finite_Set.fold F A (insert (\<lambda>\<tau>. xa) ((\<lambda>a \<tau>. a) ` Fa)) = x \<longrightarrow> \<not> (\<tau> \<Turnstile> (\<upsilon> x))") apply(simp, rule allI, rule impI)
apply(subgoal_tac "F (\<lambda>\<tau>. xa) (Finite_Set.fold F A ((\<lambda>a \<tau>. a) ` Fa)) = xc")
prefer 2
- apply(subst comp_fun_commute.fold_insert[where f = F and z = A and x = "(\<lambda>\<tau>. xa)" and A = "((\<lambda>a \<tau>. a) ` Fa)", symmetric])
- apply(rule F_commute)
+ apply(subst F_commute.fold_insert[where z = A and x = "(\<lambda>\<tau>. xa)" and A = "((\<lambda>a \<tau>. a) ` Fa)", symmetric])
apply(simp)
apply(rule image_cong)
apply(rule inject)
@@ -397,8 +396,7 @@ proof -
apply(subgoal_tac "\<not> (\<tau> \<Turnstile> (\<upsilon> (F (\<lambda>\<tau>. xa) (Finite_Set.fold F A ((\<lambda>a \<tau>. a) ` Fa)))))") apply(simp)
apply(rule F_valid_arg_false1, simp)
- apply(subst comp_fun_commute.fold_insert[where f = F and z = A and x = "(\<lambda>\<tau>. xa)" and A = "((\<lambda>a \<tau>. a) ` Fa)"])
- apply(rule F_commute)
+ apply(subst F_commute.fold_insert[where z = A and x = "(\<lambda>\<tau>. xa)" and A = "((\<lambda>a \<tau>. a) ` Fa)"])
apply(simp)
apply(rule image_cong)
apply(rule inject)
diff --git a/Citadelle/src/collection_types/UML_Bag.thy b/Citadelle/src/collection_types/UML_Bag.thy
index abdb6986931..075377d4137 100644
--- a/Citadelle/src/collection_types/UML_Bag.thy
+++ b/Citadelle/src/collection_types/UML_Bag.thy
@@ -643,7 +643,7 @@ text{* OclIncluding *}
lemma OclIncluding_valid_args_valid:
"(\<tau> \<Turnstile> \<upsilon>(X->including\<^sub>B\<^sub>a\<^sub>g(x))) = ((\<tau> \<Turnstile>(\<delta> X)) \<and> (\<tau> \<Turnstile>(\<upsilon> x)))"
-by (metis (hide_lams, no_types) OclIncluding.def_valid_then_def OclIncluding.defined_args_valid)
+by (metis (opaque_lifting, no_types) OclIncluding.def_valid_then_def OclIncluding.defined_args_valid)
lemma OclIncluding_valid_args_valid''[simp,code_unfold]:
"\<upsilon>(X->including\<^sub>B\<^sub>a\<^sub>g(x)) = ((\<delta> X) and (\<upsilon> x))"
@@ -724,7 +724,7 @@ lemma OclIsEmpty_defined_args_valid:"\<tau> \<Turnstile> \<delta> (X->isEmpty\<^
apply(case_tac "(X->size\<^sub>B\<^sub>a\<^sub>g() \<doteq> \<zero>) \<tau>", simp add: bot_option_def, simp, rename_tac x)
apply(case_tac x, simp add: null_option_def bot_option_def, simp)
apply(simp add: OclSize_def StrictRefEq\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r valid_def)
-by (metis (hide_lams, no_types)
+by (metis (opaque_lifting, no_types)
bot_fun_def OclValid_def defined_def foundation2 invalid_def)
lemma "\<tau> \<Turnstile> \<delta> (null->isEmpty\<^sub>B\<^sub>a\<^sub>g())"
@@ -743,11 +743,11 @@ by(simp add: OclSize_def StrictRefEq\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^s
text{* OclNotEmpty *}
lemma OclNotEmpty_defined_args_valid:"\<tau> \<Turnstile> \<delta> (X->notEmpty\<^sub>B\<^sub>a\<^sub>g()) \<Longrightarrow> \<tau> \<Turnstile> \<upsilon> X"
-by (metis (hide_lams, no_types) OclNotEmpty_def OclNot_defargs OclNot_not foundation6 foundation9
+by (metis (opaque_lifting, no_types) OclNotEmpty_def OclNot_defargs OclNot_not foundation6 foundation9
OclIsEmpty_defined_args_valid)
lemma "\<tau> \<Turnstile> \<delta> (null->notEmpty\<^sub>B\<^sub>a\<^sub>g())"
-by (metis (hide_lams, no_types) OclNotEmpty_def OclAnd_false1 OclAnd_idem OclIsEmpty_def
+by (metis (opaque_lifting, no_types) OclNotEmpty_def OclAnd_false1 OclAnd_idem OclIsEmpty_def
OclNot3 OclNot4 OclOr_def defined2 defined4 transform1 valid2)
lemma OclNotEmpty_infinite: "\<tau> \<Turnstile> \<delta> X \<Longrightarrow> \<not> finite (Rep_Bag_base X \<tau>) \<Longrightarrow> \<not> \<tau> \<Turnstile> \<delta> (X->notEmpty\<^sub>B\<^sub>a\<^sub>g())"
@@ -812,7 +812,7 @@ proof -
apply(frule Bag_inv_lemma[OF foundation16[THEN iffD2], OF conjI], simp)
apply(subgoal_tac "(\<delta> X) \<tau> = true \<tau>")
prefer 2
- apply (metis (hide_lams, no_types) OclValid_def foundation16)
+ apply (metis (opaque_lifting, no_types) OclValid_def foundation16)
apply(simp add: true_def,
drule OclNotEmpty_has_elt'[simplified OclValid_def true_def], simp)
apply(erule exE,
@@ -1807,7 +1807,7 @@ proof -
let ?OclSet = "\<lambda>S. \<lfloor>\<lfloor>S\<rfloor>\<rfloor> \<in> {X. X = \<bottom> \<or> X = null \<or> (\<forall>x\<in>\<lceil>\<lceil>X\<rceil>\<rceil>. x \<noteq> \<bottom>)}"
have diff_in_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e : "?OclSet ((Rep_Bag_base X \<tau>) - {x \<tau>})"
apply(simp, (rule disjI2)+)
- by (metis (hide_lams, no_types) Diff_iff Set_inv_lemma def_X)
+ by (metis (opaque_lifting, no_types) Diff_iff Set_inv_lemma def_X)
show ?thesis
apply(subst OclExcludes_def, simp add: foundation10[simplified OclValid_def] OclValid_def
@@ -1862,7 +1862,7 @@ proof -
have ins_in_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e: "\<tau> \<Turnstile> \<delta> X \<Longrightarrow> \<tau> \<Turnstile> \<upsilon> x \<Longrightarrow>
\<lfloor>\<lfloor>insert (x \<tau>) (Rep_Bag_base X \<tau>)\<rfloor>\<rfloor> \<in> {X. X = \<bottom> \<or> X = null \<or> (\<forall>x\<in>\<lceil>\<lceil>X\<rceil>\<rceil>. x \<noteq> \<bottom>)}"
apply(simp add: bot_option_def null_option_def)
- by (metis (hide_lams, no_types) Set_inv_lemma foundation18' foundation5)
+ by (metis (opaque_lifting, no_types) Set_inv_lemma foundation18' foundation5)
have m : "\<And>\<tau>. (\<lambda>_. \<bottom>) = (\<lambda>_. invalid \<tau>)" by(rule ext, simp add:invalid_def)
@@ -1877,10 +1877,10 @@ proof -
apply(drule OclSize_infinite)
apply(frule includes_def, drule includes_val, simp)
apply(subst OclSize_def, subst OclIncluding_finite_rep_set, assumption+)
- apply (metis (hide_lams, no_types) invalid_def)
+ apply (metis (opaque_lifting, no_types) invalid_def)
apply(subst OclIf_false',
- metis (hide_lams, no_types) defined5 defined6 defined_and_I defined_not_I
+ metis (opaque_lifting, no_types) defined5 defined6 defined_and_I defined_not_I
foundation1 foundation9)
apply(subst cp_OclSize, simp add: OclIncluding_includes0 cp_OclSize[symmetric])
(* *)
@@ -1900,7 +1900,7 @@ proof -
apply(subst (1 2) m[of \<tau>], simp only: OclAdd\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r.cp0[symmetric],simp, simp add:invalid_def)
apply(subst OclIncluding_finite_rep_set, fast+, simp add: OclValid_def)
(* *)
- apply(subst OclIf_false', metis (hide_lams, no_types) defined6 foundation1 foundation9
+ apply(subst OclIf_false', metis (opaque_lifting, no_types) defined6 foundation1 foundation9
OclExcluding_valid_args_valid'')
by (metis cp_OclSize foundation18' OclIncluding_valid_args_valid'' invalid_def OclSize_invalid)
qed
@@ -1972,7 +1972,7 @@ lemma OclANY_singleton_exec[simp,code_unfold]:
apply(subst (1 2) cp_OclAnd,
subst (1 2) OclNotEmpty_including[where X = "Set{}", simplified mtSet_def])
apply(simp add: mtSet_defined[simplified mtSet_def])
- apply(metis (hide_lams, no_types) finite.emptyI mtSet_def mtSet_rep_set)
+ apply(metis (opaque_lifting, no_types) finite.emptyI mtSet_def mtSet_rep_set)
apply(simp add: OclValid_def)
apply(simp add: OclIncluding_def)
apply(rule conjI)
@@ -2322,14 +2322,14 @@ proof -
(f (P (\<lambda>_. y \<tau>)) \<tau> \<or> (\<exists>x\<in>(Rep_Bag_base X \<tau>). f (P (\<lambda>_. x)) \<tau>))"
apply(simp add: OclIncluding_def OclValid_def)
apply(subst Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse, simp, (rule disjI2)+)
- by (metis (hide_lams, no_types) OclValid_def Set_inv_lemma foundation18',simp)
+ by (metis (opaque_lifting, no_types) OclValid_def Set_inv_lemma foundation18',simp)
have al_including : "\<And>f X y \<tau>. \<tau> \<Turnstile> \<delta> X \<Longrightarrow> \<tau> \<Turnstile> \<upsilon> y \<Longrightarrow>
(\<forall>x\<in>\<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X->including\<^sub>B\<^sub>a\<^sub>g(y) \<tau>)\<rceil>\<rceil>. f (P (\<lambda>_. x)) \<tau>) =
(f (P (\<lambda>_. y \<tau>)) \<tau> \<and> (\<forall>x\<in>(Rep_Bag_base X \<tau>). f (P (\<lambda>_. x)) \<tau>))"
apply(simp add: OclIncluding_def OclValid_def)
apply(subst Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse, simp, (rule disjI2)+)
- by (metis (hide_lams, no_types) OclValid_def Set_inv_lemma foundation18', simp)
+ by (metis (opaque_lifting, no_types) OclValid_def Set_inv_lemma foundation18', simp)
have ex_excluding1 : "\<And>f X y \<tau>. \<tau> \<Turnstile> \<delta> X \<Longrightarrow> \<tau> \<Turnstile> \<upsilon> y \<Longrightarrow> \<not> (f (P (\<lambda>_. y \<tau>)) \<tau>) \<Longrightarrow>
(\<exists>x\<in>(Rep_Bag_base X \<tau>). f (P (\<lambda>_. x)) \<tau>) =
@@ -2351,7 +2351,7 @@ proof -
if f (P (\<lambda>_. y \<tau>) \<tau>) then insert (y \<tau>) s else s)"
apply(simp add: OclIncluding_def OclValid_def)
apply(subst Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse, simp, (rule disjI2)+)
- apply (metis (hide_lams, no_types) OclValid_def Set_inv_lemma foundation18')
+ apply (metis (opaque_lifting, no_types) OclValid_def Set_inv_lemma foundation18')
by(simp add: Let_def, auto)
let ?OclSet = "\<lambda>S. \<lfloor>\<lfloor>S\<rfloor>\<rfloor> \<in> {X. X = \<bottom> \<or> X = null \<or> (\<forall>x\<in>\<lceil>\<lceil>X\<rceil>\<rceil>. x \<noteq> \<bottom>)}"
@@ -2363,29 +2363,29 @@ proof -
have ins_in_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e : "\<And>\<tau>. (\<delta> X) \<tau> = true \<tau> \<Longrightarrow> (\<upsilon> y) \<tau> = true \<tau> \<Longrightarrow>
?OclSet (insert (y \<tau>) {x \<in> (Rep_Bag_base X \<tau>). P (\<lambda>_. x) \<tau> \<noteq> false \<tau>})"
apply(simp, (rule disjI2)+)
- by (metis (hide_lams, no_types) OclValid_def Set_inv_lemma foundation18')
+ by (metis (opaque_lifting, no_types) OclValid_def Set_inv_lemma foundation18')
have ins_in_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e' : "\<And>\<tau>. (\<delta> X) \<tau> = true \<tau> \<Longrightarrow> (\<upsilon> y) \<tau> = true \<tau> \<Longrightarrow>
?OclSet (insert (y \<tau>) {x \<in> (Rep_Bag_base X \<tau>). x \<noteq> y \<tau> \<and> P (\<lambda>_. x) \<tau> \<noteq> false \<tau>})"
apply(simp, (rule disjI2)+)
- by (metis (hide_lams, no_types) OclValid_def Set_inv_lemma foundation18')
+ by (metis (opaque_lifting, no_types) OclValid_def Set_inv_lemma foundation18')
have ins_in_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e'' : "\<And>\<tau>. (\<delta> X) \<tau> = true \<tau> \<Longrightarrow>
?OclSet {x \<in> (Rep_Bag_base X \<tau>). P (\<lambda>_. x) \<tau> \<noteq> false \<tau>}"
apply(simp, (rule disjI2)+)
- by (metis (hide_lams, no_types) OclValid_def Set_inv_lemma)
+ by (metis (opaque_lifting, no_types) OclValid_def Set_inv_lemma)
have ins_in_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e''' : "\<And>\<tau>. (\<delta> X) \<tau> = true \<tau> \<Longrightarrow>
?OclSet {x \<in> (Rep_Bag_base X \<tau>). x \<noteq> y \<tau> \<and> P (\<lambda>_. x) \<tau> \<noteq> false \<tau>}"
apply(simp, (rule disjI2)+)
- by(metis (hide_lams, no_types) OclValid_def Set_inv_lemma)
+ by(metis (opaque_lifting, no_types) OclValid_def Set_inv_lemma)
have if_same : "\<And>a b c d \<tau>. \<tau> \<Turnstile> \<delta> a \<Longrightarrow> b \<tau> = d \<tau> \<Longrightarrow> c \<tau> = d \<tau> \<Longrightarrow>
(if a then b else c endif) \<tau> = d \<tau>"
by(simp add: OclIf_def OclValid_def)
have invert_including : "\<And>P y \<tau>. P \<tau> = \<bottom> \<Longrightarrow> P->including\<^sub>B\<^sub>a\<^sub>g(y) \<tau> = \<bottom>"
- by (metis (hide_lams, no_types) foundation16[THEN iffD1]
+ by (metis (opaque_lifting, no_types) foundation16[THEN iffD1]
foundation18' OclIncluding_valid_args_valid)
have exclude_defined : "\<And>\<tau>. \<tau> \<Turnstile> \<delta> X \<Longrightarrow>
@@ -2475,7 +2475,7 @@ proof -
apply(case_tac "\<not> (\<tau> \<Turnstile> (\<upsilon> P y))")
apply(subgoal_tac "P y \<tau> \<noteq> false \<tau>")
prefer 2
- apply (metis (hide_lams, no_types) foundation1 foundation18' valid4)
+ apply (metis (opaque_lifting, no_types) foundation1 foundation18' valid4)
apply(simp)
(* *)
apply(subst conj_comm, rule conjI)
@@ -2665,12 +2665,12 @@ proof -
have notempty': "\<And>\<tau> X. \<tau> \<Turnstile> \<delta> X \<Longrightarrow> finite (Rep_Bag_base X \<tau>) \<Longrightarrow> not (X->isEmpty\<^sub>B\<^sub>a\<^sub>g()) \<tau> \<noteq> true \<tau> \<Longrightarrow>
X \<tau> = Set{} \<tau>"
apply(case_tac "X \<tau>", rename_tac X', simp add: mtSet_def Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inject)
- apply(erule disjE, metis (hide_lams, mono_tags) bot_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def bot_option_def foundation16)
- apply(erule disjE, metis (hide_lams, no_types) bot_option_def
+ apply(erule disjE, metis (opaque_lifting, mono_tags) bot_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def bot_option_def foundation16)
+ apply(erule disjE, metis (opaque_lifting, no_types) bot_option_def
null_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def null_option_def foundation16[THEN iffD1])
- apply(case_tac X', simp, metis (hide_lams, no_types) bot_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def foundation16[THEN iffD1])
+ apply(case_tac X', simp, metis (opaque_lifting, no_types) bot_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def foundation16[THEN iffD1])
apply(rename_tac X'', case_tac X'', simp)
- apply (metis (hide_lams, no_types) foundation16[THEN iffD1] null_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def)
+ apply (metis (opaque_lifting, no_types) foundation16[THEN iffD1] null_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def)
apply(simp add: OclIsEmpty_def OclSize_def)
apply(subst (asm) cp_OclNot, subst (asm) cp_OclOr, subst (asm) StrictRefEq\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r.cp0,
subst (asm) cp_OclAnd, subst (asm) cp_OclNot)
@@ -2709,7 +2709,7 @@ proof -
apply(frule notempty'[simplified OclValid_def],
(simp add: mtSet_def Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse OclInt0_def false_def)+)
apply(drule notempty'[simplified OclValid_def], simp, simp)
- apply (metis (hide_lams, no_types) empty_iff mtSet_rep_set)
+ apply (metis (opaque_lifting, no_types) empty_iff mtSet_rep_set)
(* *)
apply(frule B)
apply(subst (1 2 3 4) cp_OclIf, simp)
@@ -2719,7 +2719,7 @@ proof -
apply(simp add: OclNotEmpty_def OclIsEmpty_def)
apply(subgoal_tac "X->size\<^sub>B\<^sub>a\<^sub>g() \<tau> = \<bottom>")
prefer 2
- apply (metis (hide_lams, no_types) OclSize_def)
+ apply (metis (opaque_lifting, no_types) OclSize_def)
apply(subst (asm) cp_OclNot, subst (asm) cp_OclOr, subst (asm) StrictRefEq\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r.cp0,
subst (asm) cp_OclAnd, subst (asm) cp_OclNot)
apply(simp add: OclValid_def foundation20[simplified OclValid_def]
diff --git a/Citadelle/src/collection_types/UML_Set.thy b/Citadelle/src/collection_types/UML_Set.thy
index ee0784eecee..8d77c9c2a22 100644
--- a/Citadelle/src/collection_types/UML_Set.thy
+++ b/Citadelle/src/collection_types/UML_Set.thy
@@ -685,7 +685,7 @@ text{* OclIncluding *}
lemma OclIncluding_valid_args_valid:
"(\<tau> \<Turnstile> \<upsilon>(X->including\<^sub>S\<^sub>e\<^sub>t(x))) = ((\<tau> \<Turnstile>(\<delta> X)) \<and> (\<tau> \<Turnstile>(\<upsilon> x)))"
-by (metis (hide_lams, no_types) OclIncluding.def_valid_then_def OclIncluding.defined_args_valid)
+by (metis (opaque_lifting, no_types) OclIncluding.def_valid_then_def OclIncluding.defined_args_valid)
lemma OclIncluding_valid_args_valid''[simp,code_unfold]:
"\<upsilon>(X->including\<^sub>S\<^sub>e\<^sub>t(x)) = ((\<delta> X) and (\<upsilon> x))"
@@ -767,7 +767,7 @@ lemma OclIsEmpty_defined_args_valid:"\<tau> \<Turnstile> \<delta> (X->isEmpty\<^
apply(case_tac "(X->size\<^sub>S\<^sub>e\<^sub>t() \<doteq> \<zero>) \<tau>", simp add: bot_option_def, simp, rename_tac x)
apply(case_tac x, simp add: null_option_def bot_option_def, simp)
apply(simp add: OclSize_def StrictRefEq\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r valid_def)
-by (metis (hide_lams, no_types)
+by (metis (opaque_lifting, no_types)
bot_fun_def OclValid_def defined_def foundation2 invalid_def)
lemma "\<tau> \<Turnstile> \<delta> (null->isEmpty\<^sub>S\<^sub>e\<^sub>t())"
@@ -786,11 +786,11 @@ by(simp add: OclSize_def StrictRefEq\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^s
text{* OclNotEmpty *}
lemma OclNotEmpty_defined_args_valid:"\<tau> \<Turnstile> \<delta> (X->notEmpty\<^sub>S\<^sub>e\<^sub>t()) \<Longrightarrow> \<tau> \<Turnstile> \<upsilon> X"
-by (metis (hide_lams, no_types) OclNotEmpty_def OclNot_defargs OclNot_not foundation6 foundation9
+by (metis (opaque_lifting, no_types) OclNotEmpty_def OclNot_defargs OclNot_not foundation6 foundation9
OclIsEmpty_defined_args_valid)
lemma "\<tau> \<Turnstile> \<delta> (null->notEmpty\<^sub>S\<^sub>e\<^sub>t())"
-by (metis (hide_lams, no_types) OclNotEmpty_def OclAnd_false1 OclAnd_idem OclIsEmpty_def
+by (metis (opaque_lifting, no_types) OclNotEmpty_def OclAnd_false1 OclAnd_idem OclIsEmpty_def
OclNot3 OclNot4 OclOr_def defined2 defined4 transform1 valid2)
lemma OclNotEmpty_infinite: "\<tau> \<Turnstile> \<delta> X \<Longrightarrow> \<not> finite \<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \<tau>)\<rceil>\<rceil> \<Longrightarrow> \<not> \<tau> \<Turnstile> \<delta> (X->notEmpty\<^sub>S\<^sub>e\<^sub>t())"
@@ -841,7 +841,7 @@ proof -
apply(frule Set_inv_lemma[OF foundation16[THEN iffD2], OF conjI], simp)
apply(subgoal_tac "(\<delta> X) \<tau> = true \<tau>")
prefer 2
- apply (metis (hide_lams, no_types) OclValid_def foundation16)
+ apply (metis (opaque_lifting, no_types) OclValid_def foundation16)
apply(simp add: true_def,
drule OclNotEmpty_has_elt[simplified OclValid_def true_def], simp)
by(erule exE,
@@ -1316,7 +1316,7 @@ proof -
show ?thesis
apply(insert excludes_def[OF assms] excludes_val[OF assms] assms,
simp add: OclExcluding_def OclExcludes_def OclIncludes_def OclNot_def OclValid_def true_def)
- by (metis (hide_lams, no_types) abs_rep_simp' assms excludes_def)
+ by (metis (opaque_lifting, no_types) abs_rep_simp' assms excludes_def)
qed
lemma OclExcluding_excludes:
@@ -1880,7 +1880,7 @@ proof -
let ?OclSet = "\<lambda>S. \<lfloor>\<lfloor>S\<rfloor>\<rfloor> \<in> {X. X = \<bottom> \<or> X = null \<or> (\<forall>x\<in>\<lceil>\<lceil>X\<rceil>\<rceil>. x \<noteq> \<bottom>)}"
have diff_in_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e : "?OclSet (\<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \<tau>)\<rceil>\<rceil> - {x \<tau>})"
apply(simp, (rule disjI2)+)
- by (metis (hide_lams, no_types) Diff_iff Set_inv_lemma def_X)
+ by (metis (opaque_lifting, no_types) Diff_iff Set_inv_lemma def_X)
show ?thesis
apply(subst OclExcludes_def, simp add: foundation10[simplified OclValid_def] OclValid_def
@@ -1935,7 +1935,7 @@ proof -
have ins_in_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e: "\<tau> \<Turnstile> \<delta> X \<Longrightarrow> \<tau> \<Turnstile> \<upsilon> x \<Longrightarrow>
\<lfloor>\<lfloor>insert (x \<tau>) \<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \<tau>)\<rceil>\<rceil>\<rfloor>\<rfloor> \<in> {X. X = \<bottom> \<or> X = null \<or> (\<forall>x\<in>\<lceil>\<lceil>X\<rceil>\<rceil>. x \<noteq> \<bottom>)}"
apply(simp add: bot_option_def null_option_def)
- by (metis (hide_lams, no_types) Set_inv_lemma foundation18' foundation5)
+ by (metis (opaque_lifting, no_types) Set_inv_lemma foundation18' foundation5)
have m : "\<And>\<tau>. (\<lambda>_. \<bottom>) = (\<lambda>_. invalid \<tau>)" by(rule ext, simp add:invalid_def)
@@ -1950,10 +1950,10 @@ proof -
apply(drule OclSize_infinite)
apply(frule includes_def, drule includes_val, simp)
apply(subst OclSize_def, subst OclIncluding_finite_rep_set, assumption+)
- apply (metis (hide_lams, no_types) invalid_def)
+ apply (metis (opaque_lifting, no_types) invalid_def)
apply(subst OclIf_false',
- metis (hide_lams, no_types) defined5 defined6 defined_and_I defined_not_I
+ metis (opaque_lifting, no_types) defined5 defined6 defined_and_I defined_not_I
foundation1 foundation9)
apply(subst cp_OclSize, simp add: OclIncluding_includes0 cp_OclSize[symmetric])
(* *)
@@ -1973,7 +1973,7 @@ proof -
apply(subst (1 2) m[of \<tau>], simp only: OclAdd\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r.cp0[symmetric],simp, simp add:invalid_def)
apply(subst OclIncluding_finite_rep_set, fast+, simp add: OclValid_def)
(* *)
- apply(subst OclIf_false', metis (hide_lams, no_types) defined6 foundation1 foundation9
+ apply(subst OclIf_false', metis (opaque_lifting, no_types) defined6 foundation1 foundation9
OclExcluding_valid_args_valid'')
by (metis cp_OclSize foundation18' OclIncluding_valid_args_valid'' invalid_def OclSize_invalid)
qed
@@ -2070,7 +2070,7 @@ lemma OclANY_singleton_exec[simp,code_unfold]:
apply(subst (1 2) cp_OclAnd,
subst (1 2) OclNotEmpty_including[where X = "Set{}", simplified mtSet_def])
apply(simp add: mtSet_defined[simplified mtSet_def])
- apply(metis (hide_lams, no_types) finite.emptyI mtSet_def mtSet_rep_set)
+ apply(metis (opaque_lifting, no_types) finite.emptyI mtSet_def mtSet_rep_set)
apply(simp add: OclValid_def)
apply(simp add: OclIncluding_def)
apply(rule conjI)
@@ -2408,6 +2408,8 @@ proof -
have inject : "inj (\<lambda>a \<tau>. a)"
by(rule inj_fun, simp)
+ interpret F_commute: comp_fun_commute "F"
+ by (fact F_commute)
show ?thesis
apply(subst (1 2) cp_OclIterate, subst OclIncluding_def, subst OclExcluding_def)
apply(case_tac "\<not> ((\<delta> S) \<tau> = true \<tau> \<and> (\<upsilon> a) \<tau> = true \<tau>)", simp add: invalid_def)
@@ -2424,7 +2426,7 @@ proof -
apply(case_tac "\<not> ((\<upsilon> A) \<tau> = true \<tau>)", (simp add: F_valid_arg)+)
apply(rule impI,
- subst Finite_Set.comp_fun_commute.fold_fun_left_comm[symmetric, OF F_commute],
+ subst F_commute.fold_fun_left_comm[symmetric],
rule remove_finite, simp)
apply(subst image_set_diff[OF inject], simp)
@@ -2432,7 +2434,7 @@ proof -
F (\<lambda>\<tau>'. a \<tau>) (Finite_Set.fold F A ((\<lambda>a \<tau>. a) ` \<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (S \<tau>)\<rceil>\<rceil> - {\<lambda>\<tau>'. a \<tau>})) \<tau>")
apply(subst F_cp, simp)
- by(subst Finite_Set.comp_fun_commute.fold_insert_remove[OF F_commute], simp+)
+ by(subst F_commute.fold_insert_remove, simp+)
qed
subsubsection{* Execution Rules on Select *}
@@ -2459,14 +2461,14 @@ proof -
(f (P (\<lambda>_. y \<tau>)) \<tau> \<or> (\<exists>x\<in>\<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \<tau>)\<rceil>\<rceil>. f (P (\<lambda>_. x)) \<tau>))"
apply(simp add: OclIncluding_def OclValid_def)
apply(subst Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse, simp, (rule disjI2)+)
- by (metis (hide_lams, no_types) OclValid_def Set_inv_lemma foundation18',simp)
+ by (metis (opaque_lifting, no_types) OclValid_def Set_inv_lemma foundation18',simp)
have al_including : "\<And>f X y \<tau>. \<tau> \<Turnstile> \<delta> X \<Longrightarrow> \<tau> \<Turnstile> \<upsilon> y \<Longrightarrow>
(\<forall>x\<in>\<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X->including\<^sub>S\<^sub>e\<^sub>t(y) \<tau>)\<rceil>\<rceil>. f (P (\<lambda>_. x)) \<tau>) =
(f (P (\<lambda>_. y \<tau>)) \<tau> \<and> (\<forall>x\<in>\<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \<tau>)\<rceil>\<rceil>. f (P (\<lambda>_. x)) \<tau>))"
apply(simp add: OclIncluding_def OclValid_def)
apply(subst Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse, simp, (rule disjI2)+)
- by (metis (hide_lams, no_types) OclValid_def Set_inv_lemma foundation18', simp)
+ by (metis (opaque_lifting, no_types) OclValid_def Set_inv_lemma foundation18', simp)
have ex_excluding1 : "\<And>f X y \<tau>. \<tau> \<Turnstile> \<delta> X \<Longrightarrow> \<tau> \<Turnstile> \<upsilon> y \<Longrightarrow> \<not> (f (P (\<lambda>_. y \<tau>)) \<tau>) \<Longrightarrow>
(\<exists>x\<in>\<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \<tau>)\<rceil>\<rceil>. f (P (\<lambda>_. x)) \<tau>) =
@@ -2488,7 +2490,7 @@ proof -
if f (P (\<lambda>_. y \<tau>) \<tau>) then insert (y \<tau>) s else s)"
apply(simp add: OclIncluding_def OclValid_def)
apply(subst Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse, simp, (rule disjI2)+)
- apply (metis (hide_lams, no_types) OclValid_def Set_inv_lemma foundation18')
+ apply (metis (opaque_lifting, no_types) OclValid_def Set_inv_lemma foundation18')
by(simp add: Let_def, auto)
let ?OclSet = "\<lambda>S. \<lfloor>\<lfloor>S\<rfloor>\<rfloor> \<in> {X. X = \<bottom> \<or> X = null \<or> (\<forall>x\<in>\<lceil>\<lceil>X\<rceil>\<rceil>. x \<noteq> \<bottom>)}"
@@ -2500,29 +2502,29 @@ proof -
have ins_in_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e : "\<And>\<tau>. (\<delta> X) \<tau> = true \<tau> \<Longrightarrow> (\<upsilon> y) \<tau> = true \<tau> \<Longrightarrow>
?OclSet (insert (y \<tau>) {x \<in> \<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \<tau>)\<rceil>\<rceil>. P (\<lambda>_. x) \<tau> \<noteq> false \<tau>})"
apply(simp, (rule disjI2)+)
- by (metis (hide_lams, no_types) OclValid_def Set_inv_lemma foundation18')
+ by (metis (opaque_lifting, no_types) OclValid_def Set_inv_lemma foundation18')
have ins_in_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e' : "\<And>\<tau>. (\<delta> X) \<tau> = true \<tau> \<Longrightarrow> (\<upsilon> y) \<tau> = true \<tau> \<Longrightarrow>
?OclSet (insert (y \<tau>) {x \<in> \<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \<tau>)\<rceil>\<rceil>. x \<noteq> y \<tau> \<and> P (\<lambda>_. x) \<tau> \<noteq> false \<tau>})"
apply(simp, (rule disjI2)+)
- by (metis (hide_lams, no_types) OclValid_def Set_inv_lemma foundation18')
+ by (metis (opaque_lifting, no_types) OclValid_def Set_inv_lemma foundation18')
have ins_in_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e'' : "\<And>\<tau>. (\<delta> X) \<tau> = true \<tau> \<Longrightarrow>
?OclSet {x \<in> \<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \<tau>)\<rceil>\<rceil>. P (\<lambda>_. x) \<tau> \<noteq> false \<tau>}"
apply(simp, (rule disjI2)+)
- by (metis (hide_lams, no_types) OclValid_def Set_inv_lemma)
+ by (metis (opaque_lifting, no_types) OclValid_def Set_inv_lemma)
have ins_in_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e''' : "\<And>\<tau>. (\<delta> X) \<tau> = true \<tau> \<Longrightarrow>
?OclSet {x \<in> \<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \<tau>)\<rceil>\<rceil>. x \<noteq> y \<tau> \<and> P (\<lambda>_. x) \<tau> \<noteq> false \<tau>}"
apply(simp, (rule disjI2)+)
- by(metis (hide_lams, no_types) OclValid_def Set_inv_lemma)
+ by(metis (opaque_lifting, no_types) OclValid_def Set_inv_lemma)
have if_same : "\<And>a b c d \<tau>. \<tau> \<Turnstile> \<delta> a \<Longrightarrow> b \<tau> = d \<tau> \<Longrightarrow> c \<tau> = d \<tau> \<Longrightarrow>
(if a then b else c endif) \<tau> = d \<tau>"
by(simp add: OclIf_def OclValid_def)
have invert_including : "\<And>P y \<tau>. P \<tau> = \<bottom> \<Longrightarrow> P->including\<^sub>S\<^sub>e\<^sub>t(y) \<tau> = \<bottom>"
- by (metis (hide_lams, no_types) foundation16[THEN iffD1]
+ by (metis (opaque_lifting, no_types) foundation16[THEN iffD1]
foundation18' OclIncluding_valid_args_valid)
have exclude_defined : "\<And>\<tau>. \<tau> \<Turnstile> \<delta> X \<Longrightarrow>
@@ -2612,7 +2614,7 @@ proof -
apply(case_tac "\<not> (\<tau> \<Turnstile> (\<upsilon> P y))")
apply(subgoal_tac "P y \<tau> \<noteq> false \<tau>")
prefer 2
- apply (metis (hide_lams, no_types) foundation1 foundation18' valid4)
+ apply (metis (opaque_lifting, no_types) foundation1 foundation18' valid4)
apply(simp)
(* *)
apply(subst conj_comm, rule conjI)
@@ -2802,12 +2804,12 @@ proof -
have notempty': "\<And>\<tau> X. \<tau> \<Turnstile> \<delta> X \<Longrightarrow> finite \<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (X \<tau>)\<rceil>\<rceil> \<Longrightarrow> not (X->isEmpty\<^sub>S\<^sub>e\<^sub>t()) \<tau> \<noteq> true \<tau> \<Longrightarrow>
X \<tau> = Set{} \<tau>"
apply(case_tac "X \<tau>", rename_tac X', simp add: mtSet_def Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inject)
- apply(erule disjE, metis (hide_lams, mono_tags) bot_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def bot_option_def foundation16)
- apply(erule disjE, metis (hide_lams, no_types) bot_option_def
+ apply(erule disjE, metis (opaque_lifting, mono_tags) bot_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def bot_option_def foundation16)
+ apply(erule disjE, metis (opaque_lifting, no_types) bot_option_def
null_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def null_option_def foundation16[THEN iffD1])
- apply(case_tac X', simp, metis (hide_lams, no_types) bot_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def foundation16[THEN iffD1])
+ apply(case_tac X', simp, metis (opaque_lifting, no_types) bot_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def foundation16[THEN iffD1])
apply(rename_tac X'', case_tac X'', simp)
- apply (metis (hide_lams, no_types) foundation16[THEN iffD1] null_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def)
+ apply (metis (opaque_lifting, no_types) foundation16[THEN iffD1] null_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_def)
apply(simp add: OclIsEmpty_def OclSize_def)
apply(subst (asm) cp_OclNot, subst (asm) cp_OclOr, subst (asm) StrictRefEq\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r.cp0,
subst (asm) cp_OclAnd, subst (asm) cp_OclNot)
@@ -2846,7 +2848,7 @@ proof -
apply(frule notempty'[simplified OclValid_def],
(simp add: mtSet_def Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse OclInt0_def false_def)+)
apply(drule notempty'[simplified OclValid_def], simp, simp)
- apply (metis (hide_lams, no_types) empty_iff mtSet_rep_set)
+ apply (metis (opaque_lifting, no_types) empty_iff mtSet_rep_set)
(* *)
apply(frule B)
apply(subst (1 2 3 4) cp_OclIf, simp)
@@ -2856,7 +2858,7 @@ proof -
apply(simp add: OclNotEmpty_def OclIsEmpty_def)
apply(subgoal_tac "X->size\<^sub>S\<^sub>e\<^sub>t() \<tau> = \<bottom>")
prefer 2
- apply (metis (hide_lams, no_types) OclSize_def)
+ apply (metis (opaque_lifting, no_types) OclSize_def)
apply(subst (asm) cp_OclNot, subst (asm) cp_OclOr, subst (asm) StrictRefEq\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r.cp0,
subst (asm) cp_OclAnd, subst (asm) cp_OclNot)
apply(simp add: OclValid_def foundation20[simplified OclValid_def]
@@ -3034,9 +3036,9 @@ lemma OclForall_iterate:
assumes S_finite: "finite \<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (S \<tau>)\<rceil>\<rceil>"
shows "S->forAll\<^sub>S\<^sub>e\<^sub>t(x | P x) \<tau> = (S->iterate\<^sub>S\<^sub>e\<^sub>t(x; acc = true | acc and P x)) \<tau>"
proof -
- have and_comm : "comp_fun_commute (\<lambda>x acc. acc and P x)"
+ interpret and_comm: comp_fun_commute "(\<lambda>x acc. acc and P x)"
apply(simp add: comp_fun_commute_def comp_def)
- by (metis OclAnd_assoc OclAnd_commute)
+ by (metis OclAnd_assoc OclAnd_commute)
have ex_insert : "\<And>x F P. (\<exists>x\<in>insert x F. P x) = (P x \<or> (\<exists>x\<in>F. P x))"
by (metis insert_iff)
@@ -3066,13 +3068,13 @@ proof -
apply(rule finite_ne_induct[OF S_finite], simp)
(* *)
apply(simp only: image_insert)
- apply(subst comp_fun_commute.fold_insert[OF and_comm], simp)
+ apply(subst and_comm.fold_insert, simp)
apply (metis empty_iff image_empty)
apply(simp add: invalid_def)
apply (metis bot_fun_def destruct_ocl null_fun_def)
(* *)
apply(simp only: image_insert)
- apply(subst comp_fun_commute.fold_insert[OF and_comm], simp)
+ apply(subst and_comm.fold_insert, simp)
apply (metis (mono_tags) imageE)
(* *)
diff --git a/Citadelle/src/compiler/Generator_dynamic_sequential.thy b/Citadelle/src/compiler/Generator_dynamic_sequential.thy
index 8028479f78c..1db21686bcb 100644
--- a/Citadelle/src/compiler/Generator_dynamic_sequential.thy
+++ b/Citadelle/src/compiler/Generator_dynamic_sequential.thy
@@ -508,7 +508,7 @@ fun type_synonym top (Type_synonym ((n, v), l)) = #theory top (fn thy => let val
(Isabelle_Typedecl.abbrev_cmd0 (SOME s_bind) thy (of_semi__typ l))) thy end)
fun type_notation top (Type_notation (n, e)) = #local_theory top NONE NONE
- (Specification.type_notation_cmd true ("", true) [(To_string0 n, Mixfix (Input.string (To_string0 e), [], 1000, Position.no_range))])
+ (Local_Theory.type_notation_cmd true ("", true) [(To_string0 n, Mixfix (Input.string (To_string0 e), [], 1000, Position.no_range))])
fun instantiation1 name thy = thy
|> Class.instantiation ([ let val Term.Type (s, _) = Isabelle_Typedecl.abbrev_cmd0 NONE thy name in s end ],
@@ -584,6 +584,11 @@ fun section n s _ =
out_intensify (mk (Markup.markup Markup.keyword3 (To_string0 s)) n) ""
end
+fun text name s =
+ Document_Output.document_output
+ {markdown = true, markup = fn body => [XML.Elem (Markup.latex_body name, body)]}
+ (NONE, Input.string (To_string0 s))
+
fun ml top (SMLa ml) = #generic_theory top
(ML_Context.exec let val source = input_source ml in
fn () => ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source
@@ -669,18 +674,27 @@ fun semi__theory (top : ('transitionM, 'transitionM, 'state) toplevel) = let ope
| Theory_axiomatization axiomatization =>
cons (\<^command_keyword>\<open>axiomatization\<close>, Cmd.axiomatization top axiomatization)
| Theory_section (Section (n, s)) => let val n = To_nat n in fn st => st
- |>:: (case n of 0 =>
+ |>:: let val (name, pos) = case n of 0 =>
\<^command_keyword>\<open>section\<close> | 1 =>
\<^command_keyword>\<open>subsection\<close> | _ =>
- \<^command_keyword>\<open>subsubsection\<close>,
- #tr_raw top (Pure_Syn.document_command {markdown = false} (NONE, Input.string (To_string0 s))))
+ \<^command_keyword>\<open>subsubsection\<close>
+ in
+ ( (name, pos)
+ , #tr_raw
+ top
+ (Document_Output.document_output
+ {markdown = false, markup = fn body => [XML.Elem (Markup.latex_heading name, body)]}
+ (NONE, Input.string (To_string0 s))))
+ end
|>:: (\<^command_keyword>\<open>print_syntax\<close>, #keep top (Cmd.section n s)) end
| Theory_text (Text s) =>
- cons (\<^command_keyword>\<open>text\<close>,
- #tr_raw top (Pure_Syn.document_command {markdown = true} (NONE, Input.string (To_string0 s))))
+ cons let val (name, pos) =
+ \<^command_keyword>\<open>text\<close>
+ in ((name, pos), #tr_raw top (Cmd.text name s)) end
| Theory_text_raw (Text_raw s) =>
- cons (\<^command_keyword>\<open>text_raw\<close>,
- #tr_raw top (Pure_Syn.document_command {markdown = true} (NONE, Input.string (To_string0 s))))
+ cons let val (name, pos) =
+ \<^command_keyword>\<open>text_raw\<close>
+ in ((name, pos), #tr_raw top (Cmd.text name s)) end
| Theory_ML ml =>
cons (\<^command_keyword>\<open>ML\<close>, Cmd.ml top ml)
| Theory_setup setup =>
@@ -777,7 +791,6 @@ structure Meta_Cmd_Data = Theory_Data
(open META
type T = T
val empty = []
- val extend = I
val merge = #2)
fun ML_context_exec pos ants =
@@ -793,7 +806,7 @@ fun meta_command0 s_put f_get constraint source =
Context.Theory
#> ML_context_exec (Input.pos_of source)
(ML_Lex.read "let open META val ML = META.SML val "
- @ ML_Lex.read_set_range (Input.range_of source) name
+ @ ML_Lex.read_range (Input.range_of source) name
@ ML_Lex.read (" : " ^ constraint ^ " = ")
@ ML_Lex.read_source source
@ ML_Lex.read (" in Context.>> (Context.map_theory (" ^ s_put ^ " " ^ name ^ ")) end"))
@@ -974,7 +987,6 @@ type T = (unit META.compiler_env_config_ext, theory) generation_mode
structure Data_gen = Theory_Data
(type T = T
val empty = {deep = [], shallow = [], syntax_print = [NONE]}
- val extend = I
fun merge (e1, e2) = { deep = #deep e1 @ #deep e2
, shallow = #shallow e1 @ #shallow e2
, syntax_print = #syntax_print e1 @ #syntax_print e2 })
@@ -1083,7 +1095,7 @@ fun meta_command0 s_put f_get f_get0 constraint source =
Context.Theory
#> Bind_META.ML_context_exec (Input.pos_of source)
(ML_Lex.read "let open META val ML = META.SML val "
- @ ML_Lex.read_set_range (Input.range_of source) name
+ @ ML_Lex.read_range (Input.range_of source) name
@ ML_Lex.read (" : " ^ constraint ^ " = ")
@ ML_Lex.read_source source
@ ML_Lex.read (" in Context.>> (Context.map_theory (fn thy => " ^ s_put ^ " (" ^ name ^ " (" ^ f_get0 ^ " thy)) thy)) end"))
@@ -1949,7 +1961,6 @@ end
structure Haskabelle_Data = Theory_Data
(type T = Haskabelle_Data_T
val empty = ([], [])
- val extend = I
val merge = #2)
local
@@ -1960,7 +1971,7 @@ in
fun parse meta_parse_shallow meta_parse_imports meta_parse_code meta_parse_functions hsk_name check_dir hsk_str ((((((((old_datatype, try_import), only_types), ignore_not_in_scope), abstract_mutual_data_params), concat_modules), base_path_abs), l_rewrite), source) thy =
let fun string_of_bool b = if b then "true" else "false"
val st =
- Bash.process
+ (Isabelle_System.bash_process o Bash.script)
(space_implode " "
( [ Path.implode haskabelle_bin
, "--internal", Path.implode haskabelle_default
@@ -1983,8 +1994,8 @@ in
([], [ Resources'.check_file (Proof_Context.init_global thy) (SOME Path.current) source ])
of (cts, files) => List.concat [ ["--hsk-contents"], cts, ["--files"], files ])))
in
- if #rc st = 0 then
- Bind_META.meta_command0 "Haskabelle_Data.put" Haskabelle_Data.get "Haskabelle_Data_T" (Input.string (#out st)) thy
+ if Process_Result.rc st = 0 then
+ Bind_META.meta_command0 "Haskabelle_Data.put" Haskabelle_Data.get "Haskabelle_Data_T" (Input.string (Process_Result.out st)) thy
|> (fn (l_mod, l_rep) =>
let
val _ =
@@ -1993,7 +2004,7 @@ in
let fun advance_offset n =
if n = 0 then I
else fn (x :: xs, p) =>
- advance_offset (n - String.size x) (xs, Position.advance x p)
+ advance_offset (n - String.size x) (xs, Position.symbol x p)
val l_rep =
fold (fn ((offset, end_offset), (markup, prop)) => fn (content, (pos, pos_o), acc) =>
let val offset = To_nat offset
@@ -2017,12 +2028,14 @@ in
, From.string (Context.theory_name thy)
, (m, concat_modules)))
|> META.META_haskell end)
- |> tap (fn _ => warning (#err st))
+ |> tap (fn _ => warning (Process_Result.err st))
else
- let val _ = #terminate st ()
- in error (if #err st = "" then
- "Failed executing the ML process (" ^ Int.toString (#rc st) ^ ")"
- else #err st |> String.explode |> trim (fn #"\n" => true | _ => false) |> String.implode) end
+ error (if Process_Result.err st = "" then
+ "Failed executing the ML process (" ^ Int.toString (Process_Result.rc st) ^ ")"
+ else
+ Process_Result.err st |> String.explode
+ |> trim (fn #"\n" => true | _ => false)
+ |> String.implode)
end
val parse' = parse false [] NONE META.Gen_no_apply NONE Resources'.check_dir
end
@@ -2035,7 +2048,6 @@ local
structure Data_lang = Theory_Data
(type T = (haskell_parse * string option * (bool * string) list * string * (META.abr_string -> META.gen_meta)) Name_Space.table
val empty = Name_Space.empty_table "meta_language"
- val extend = I
val merge = Name_Space.merge_tables)
structure Parse' =
diff --git a/Citadelle/src/compiler_citadelle/Generator_dynamic_concurrent.thy b/Citadelle/src/compiler_citadelle/Generator_dynamic_concurrent.thy
index 641ae8e8f65..4fdcdcebc3e 100644
--- a/Citadelle/src/compiler_citadelle/Generator_dynamic_concurrent.thy
+++ b/Citadelle/src/compiler_citadelle/Generator_dynamic_concurrent.thy
@@ -486,7 +486,7 @@ fun type_synonym top (Type_synonym ((n, v), l)) = #theory top (fn thy => let val
(Isabelle_Typedecl.abbrev_cmd0 (SOME s_bind) thy (of_semi__typ l))) thy end)
fun type_notation top (Type_notation (n, e)) = #local_theory top NONE NONE
- (Specification.type_notation_cmd true ("", true) [(To_string0 n, Mixfix (Input.string (To_string0 e), [], 1000, Position.no_range))])
+ (Local_Theory.type_notation_cmd true ("", true) [(To_string0 n, Mixfix (Input.string (To_string0 e), [], 1000, Position.no_range))])
fun instantiation1 name thy = thy
|> Class.instantiation ([ let val Term.Type (s, _) = Isabelle_Typedecl.abbrev_cmd0 NONE thy name in s end ],
@@ -562,6 +562,11 @@ fun section n s _ =
out_intensify (mk (Markup.markup Markup.keyword3 (To_string0 s)) n) ""
end
+fun text name s =
+ Document_Output.document_output
+ {markdown = true, markup = fn body => [XML.Elem (Markup.latex_body name, body)]}
+ (NONE, Input.string (To_string0 s))
+
fun ml top (SMLa ml) = #generic_theory top
(ML_Context.exec let val source = input_source ml in
fn () => ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source
@@ -647,18 +652,27 @@ fun semi__theory (top : ('transitionM, 'transitionM, 'state) toplevel) = let ope
| Theory_axiomatization axiomatization =>
cons (\<^command_keyword>\<open>axiomatization\<close>, Cmd.axiomatization top axiomatization)
| Theory_section (Section (n, s)) => let val n = To_nat n in fn st => st
- |>:: (case n of 0 =>
+ |>:: let val (name, pos) = case n of 0 =>
\<^command_keyword>\<open>section\<close> | 1 =>
\<^command_keyword>\<open>subsection\<close> | _ =>
- \<^command_keyword>\<open>subsubsection\<close>,
- #tr_raw top (Pure_Syn.document_command {markdown = false} (NONE, Input.string (To_string0 s))))
+ \<^command_keyword>\<open>subsubsection\<close>
+ in
+ ( (name, pos)
+ , #tr_raw
+ top
+ (Document_Output.document_output
+ {markdown = false, markup = fn body => [XML.Elem (Markup.latex_heading name, body)]}
+ (NONE, Input.string (To_string0 s))))
+ end
|>:: (\<^command_keyword>\<open>print_syntax\<close>, #keep top (Cmd.section n s)) end
| Theory_text (Text s) =>
- cons (\<^command_keyword>\<open>text\<close>,
- #tr_raw top (Pure_Syn.document_command {markdown = true} (NONE, Input.string (To_string0 s))))
+ cons let val (name, pos) =
+ \<^command_keyword>\<open>text\<close>
+ in ((name, pos), #tr_raw top (Cmd.text name s)) end
| Theory_text_raw (Text_raw s) =>
- cons (\<^command_keyword>\<open>text_raw\<close>,
- #tr_raw top (Pure_Syn.document_command {markdown = true} (NONE, Input.string (To_string0 s))))
+ cons let val (name, pos) =
+ \<^command_keyword>\<open>text_raw\<close>
+ in ((name, pos), #tr_raw top (Cmd.text name s)) end
| Theory_ML ml =>
cons (\<^command_keyword>\<open>ML\<close>, Cmd.ml top ml)
| Theory_setup setup =>
@@ -755,7 +769,6 @@ structure Meta_Cmd_Data = Theory_Data
(open META
type T = T
val empty = []
- val extend = I
val merge = #2)
fun ML_context_exec pos ants =
@@ -771,7 +784,7 @@ fun meta_command0 s_put f_get constraint source =
Context.Theory
#> ML_context_exec (Input.pos_of source)
(ML_Lex.read "let open META val ML = META.SML val "
- @ ML_Lex.read_set_range (Input.range_of source) name
+ @ ML_Lex.read_range (Input.range_of source) name
@ ML_Lex.read (" : " ^ constraint ^ " = ")
@ ML_Lex.read_source source
@ ML_Lex.read (" in Context.>> (Context.map_theory (" ^ s_put ^ " " ^ name ^ ")) end"))
@@ -952,7 +965,6 @@ type T = (unit META.compiler_env_config_ext, theory) generation_mode
structure Data_gen = Theory_Data
(type T = T
val empty = {deep = [], shallow = [], syntax_print = [NONE]}
- val extend = I
fun merge (e1, e2) = { deep = #deep e1 @ #deep e2
, shallow = #shallow e1 @ #shallow e2
, syntax_print = #syntax_print e1 @ #syntax_print e2 })
@@ -1061,7 +1073,7 @@ fun meta_command0 s_put f_get f_get0 constraint source =
Context.Theory
#> Bind_META.ML_context_exec (Input.pos_of source)
(ML_Lex.read "let open META val ML = META.SML val "
- @ ML_Lex.read_set_range (Input.range_of source) name
+ @ ML_Lex.read_range (Input.range_of source) name
@ ML_Lex.read (" : " ^ constraint ^ " = ")
@ ML_Lex.read_source source
@ ML_Lex.read (" in Context.>> (Context.map_theory (fn thy => " ^ s_put ^ " (" ^ name ^ " (" ^ f_get0 ^ " thy)) thy)) end"))
@@ -1927,7 +1939,6 @@ end
structure Haskabelle_Data = Theory_Data
(type T = Haskabelle_Data_T
val empty = ([], [])
- val extend = I
val merge = #2)
local
@@ -1938,7 +1949,7 @@ in
fun parse meta_parse_shallow meta_parse_imports meta_parse_code meta_parse_functions hsk_name check_dir hsk_str ((((((((old_datatype, try_import), only_types), ignore_not_in_scope), abstract_mutual_data_params), concat_modules), base_path_abs), l_rewrite), source) thy =
let fun string_of_bool b = if b then "true" else "false"
val st =
- Bash.process
+ (Isabelle_System.bash_process o Bash.script)
(space_implode " "
( [ Path.implode haskabelle_bin
, "--internal", Path.implode haskabelle_default
@@ -1961,8 +1972,8 @@ in
([], [ Resources'.check_file (Proof_Context.init_global thy) (SOME Path.current) source ])
of (cts, files) => List.concat [ ["--hsk-contents"], cts, ["--files"], files ])))
in
- if #rc st = 0 then
- Bind_META.meta_command0 "Haskabelle_Data.put" Haskabelle_Data.get "Haskabelle_Data_T" (Input.string (#out st)) thy
+ if Process_Result.rc st = 0 then
+ Bind_META.meta_command0 "Haskabelle_Data.put" Haskabelle_Data.get "Haskabelle_Data_T" (Input.string (Process_Result.out st)) thy
|> (fn (l_mod, l_rep) =>
let
val _ =
@@ -1971,7 +1982,7 @@ in
let fun advance_offset n =
if n = 0 then I
else fn (x :: xs, p) =>
- advance_offset (n - String.size x) (xs, Position.advance x p)
+ advance_offset (n - String.size x) (xs, Position.symbol x p)
val l_rep =
fold (fn ((offset, end_offset), (markup, prop)) => fn (content, (pos, pos_o), acc) =>
let val offset = To_nat offset
@@ -1995,12 +2006,14 @@ in
, From.string (Context.theory_name thy)
, (m, concat_modules)))
|> META.META_haskell end)
- |> tap (fn _ => warning (#err st))
+ |> tap (fn _ => warning (Process_Result.err st))
else
- let val _ = #terminate st ()
- in error (if #err st = "" then
- "Failed executing the ML process (" ^ Int.toString (#rc st) ^ ")"
- else #err st |> String.explode |> trim (fn #"\n" => true | _ => false) |> String.implode) end
+ error (if Process_Result.err st = "" then
+ "Failed executing the ML process (" ^ Int.toString (Process_Result.rc st) ^ ")"
+ else
+ Process_Result.err st |> String.explode
+ |> trim (fn #"\n" => true | _ => false)
+ |> String.implode)
end
val parse' = parse false [] NONE META.Gen_no_apply NONE Resources'.check_dir
end
@@ -2013,7 +2026,6 @@ local
structure Data_lang = Theory_Data
(type T = (haskell_parse * string option * (bool * string) list * string * (META.abr_string -> META.gen_meta)) Name_Space.table
val empty = Name_Space.empty_table "meta_language"
- val extend = I
val merge = Name_Space.merge_tables)
structure Parse' =
diff --git a/Citadelle/src/compiler_citadelle/Generator_dynamic_export_testing.thy b/Citadelle/src/compiler_citadelle/Generator_dynamic_export_testing.thy
index 59a009ae99b..ecb6cde8aa7 100644
--- a/Citadelle/src/compiler_citadelle/Generator_dynamic_export_testing.thy
+++ b/Citadelle/src/compiler_citadelle/Generator_dynamic_export_testing.thy
@@ -494,7 +494,7 @@ fun type_synonym top (Type_synonym ((n, v), l)) = #theory top (fn thy => let val
(Isabelle_Typedecl.abbrev_cmd0 (SOME s_bind) thy (of_semi__typ l))) thy end)
fun type_notation top (Type_notation (n, e)) = #local_theory top NONE NONE
- (Specification.type_notation_cmd true ("", true) [(To_string0 n, Mixfix (Input.string (To_string0 e), [], 1000, Position.no_range))])
+ (Local_Theory.type_notation_cmd true ("", true) [(To_string0 n, Mixfix (Input.string (To_string0 e), [], 1000, Position.no_range))])
fun instantiation1 name thy = thy
|> Class.instantiation ([ let val Term.Type (s, _) = Isabelle_Typedecl.abbrev_cmd0 NONE thy name in s end ],
@@ -570,6 +570,11 @@ fun section n s _ =
out_intensify (mk (Markup.markup Markup.keyword3 (To_string0 s)) n) ""
end
+fun text name s =
+ Document_Output.document_output
+ {markdown = true, markup = fn body => [XML.Elem (Markup.latex_body name, body)]}
+ (NONE, Input.string (To_string0 s))
+
fun ml top (SMLa ml) = #generic_theory top
(ML_Context.exec let val source = input_source ml in
fn () => ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source
@@ -655,18 +660,27 @@ fun semi__theory (top : ('transitionM, 'transitionM, 'state) toplevel) = let ope
| Theory_axiomatization axiomatization =>
cons (\<^command_keyword>\<open>axiomatization\<close>, Cmd.axiomatization top axiomatization)
| Theory_section (Section (n, s)) => let val n = To_nat n in fn st => st
- |>:: (case n of 0 =>
+ |>:: let val (name, pos) = case n of 0 =>
\<^command_keyword>\<open>section\<close> | 1 =>
\<^command_keyword>\<open>subsection\<close> | _ =>
- \<^command_keyword>\<open>subsubsection\<close>,
- #tr_raw top (Pure_Syn.document_command {markdown = false} (NONE, Input.string (To_string0 s))))
+ \<^command_keyword>\<open>subsubsection\<close>
+ in
+ ( (name, pos)
+ , #tr_raw
+ top
+ (Document_Output.document_output
+ {markdown = false, markup = fn body => [XML.Elem (Markup.latex_heading name, body)]}
+ (NONE, Input.string (To_string0 s))))
+ end
|>:: (\<^command_keyword>\<open>print_syntax\<close>, #keep top (Cmd.section n s)) end
| Theory_text (Text s) =>
- cons (\<^command_keyword>\<open>text\<close>,
- #tr_raw top (Pure_Syn.document_command {markdown = true} (NONE, Input.string (To_string0 s))))
+ cons let val (name, pos) =
+ \<^command_keyword>\<open>text\<close>
+ in ((name, pos), #tr_raw top (Cmd.text name s)) end
| Theory_text_raw (Text_raw s) =>
- cons (\<^command_keyword>\<open>text_raw\<close>,
- #tr_raw top (Pure_Syn.document_command {markdown = true} (NONE, Input.string (To_string0 s))))
+ cons let val (name, pos) =
+ \<^command_keyword>\<open>text_raw\<close>
+ in ((name, pos), #tr_raw top (Cmd.text name s)) end
| Theory_ML ml =>
cons (\<^command_keyword>\<open>ML\<close>, Cmd.ml top ml)
| Theory_setup setup =>
@@ -763,7 +777,6 @@ structure Meta_Cmd_Data = Theory_Data
(open META
type T = T
val empty = []
- val extend = I
val merge = #2)
fun ML_context_exec pos ants =
@@ -779,7 +792,7 @@ fun meta_command0 s_put f_get constraint source =
Context.Theory
#> ML_context_exec (Input.pos_of source)
(ML_Lex.read "let open META val ML = META.SML val "
- @ ML_Lex.read_set_range (Input.range_of source) name
+ @ ML_Lex.read_range (Input.range_of source) name
@ ML_Lex.read (" : " ^ constraint ^ " = ")
@ ML_Lex.read_source source
@ ML_Lex.read (" in Context.>> (Context.map_theory (" ^ s_put ^ " " ^ name ^ ")) end"))
@@ -954,10 +967,11 @@ structure Export_code_env = struct
end
fun compile l cmd =
- let val (l, rc) = fold (fn cmd => (fn (l, 0) =>
- let val {out, err, rc, ...} = Bash.process cmd in
- ((out, err) :: l, rc) end
- | x => x)) l ([], 0)
+ let val (l, rc) = fold (fn cmd =>
+ (fn (l, 0) =>
+ let val res = Isabelle_System.bash_process (Bash.script cmd) in
+ ((Process_Result.out res, Process_Result.err res) :: l, Process_Result.rc res) end
+ | x => x)) l ([], 0)
val l = rev l in
if rc = 0 then
(l, Isabelle_System.bash_output cmd)
@@ -1279,7 +1293,6 @@ type T = (unit META.compiler_env_config_ext, theory) generation_mode
structure Data_gen = Theory_Data
(type T = T
val empty = {deep = [], shallow = [], syntax_print = [NONE]}
- val extend = I
fun merge (e1, e2) = { deep = #deep e1 @ #deep e2
, shallow = #shallow e1 @ #shallow e2
, syntax_print = #syntax_print e1 @ #syntax_print e2 })
@@ -1369,7 +1382,7 @@ fun f_command l_mode =
let val tmp_export_code = Deep.mk_path_export_code (#tmp_export_code i_deep) ml_compiler i
fun mk_fic s = Path.append tmp_export_code (Path.make [s])
val () = Deep0.Find.check_compil ml_compiler ()
- val () = Isabelle_System.mkdir(*TODO?*) tmp_export_code in
+ val _ = Isabelle_System.make_directory(*TODO?*) tmp_export_code in
(( ( (ml_compiler, ml_module)
, ( Path.implode (if Deep0.Find.export_mode ml_compiler = Deep0.Export_code_env.Directory then
tmp_export_code
@@ -1416,7 +1429,7 @@ fun meta_command0 s_put f_get f_get0 constraint source =
Context.Theory
#> Bind_META.ML_context_exec (Input.pos_of source)
(ML_Lex.read "let open META val ML = META.SML val "
- @ ML_Lex.read_set_range (Input.range_of source) name
+ @ ML_Lex.read_range (Input.range_of source) name
@ ML_Lex.read (" : " ^ constraint ^ " = ")
@ ML_Lex.read_source source
@ ML_Lex.read (" in Context.>> (Context.map_theory (fn thy => " ^ s_put ^ " (" ^ name ^ " (" ^ f_get0 ^ " thy)) thy)) end"))
diff --git a/Citadelle/src/compiler_generic/meta_isabelle/Meta_Isabelle.thy b/Citadelle/src/compiler_generic/meta_isabelle/Meta_Isabelle.thy
index 4004f720950..71e26dea977 100644
--- a/Citadelle/src/compiler_generic/meta_isabelle/Meta_Isabelle.thy
+++ b/Citadelle/src/compiler_generic/meta_isabelle/Meta_Isabelle.thy
@@ -336,7 +336,7 @@ definition "subst_l = Method_subst_l"
definition insert where "insert = Method_insert o L.map Thms_single"
definition plus where "plus = Method_plus"
definition "option = Method_option"
-definition "or = Method_or"
+definition or where "or = Method_or"
definition "meth_gen_simp = Method_simp_add_del [] []"
definition "meth_gen_simp_add2 l1 l2 = Method_simp_add_del (L.flatten [ L.map Thms_mult l1
, L.map (Thms_single o Thm_thm) l2])
diff --git a/Citadelle/src/compiler_generic/toy_example/embedding/Generator_dynamic_sequential.thy b/Citadelle/src/compiler_generic/toy_example/embedding/Generator_dynamic_sequential.thy
index 6b36a5b78e7..1eb667278c6 100644
--- a/Citadelle/src/compiler_generic/toy_example/embedding/Generator_dynamic_sequential.thy
+++ b/Citadelle/src/compiler_generic/toy_example/embedding/Generator_dynamic_sequential.thy
@@ -478,7 +478,7 @@ fun type_synonym top (Type_synonym ((n, v), l)) = #theory top (fn thy => let val
(Isabelle_Typedecl.abbrev_cmd0 (SOME s_bind) thy (of_semi__typ l))) thy end)
fun type_notation top (Type_notation (n, e)) = #local_theory top NONE NONE
- (Specification.type_notation_cmd true ("", true) [(To_string0 n, Mixfix (Input.string (To_string0 e), [], 1000, Position.no_range))])
+ (Local_Theory.type_notation_cmd true ("", true) [(To_string0 n, Mixfix (Input.string (To_string0 e), [], 1000, Position.no_range))])
fun instantiation1 name thy = thy
|> Class.instantiation ([ let val Term.Type (s, _) = Isabelle_Typedecl.abbrev_cmd0 NONE thy name in s end ],
@@ -554,6 +554,11 @@ fun section n s _ =
out_intensify (mk (Markup.markup Markup.keyword3 (To_string0 s)) n) ""
end
+fun text name s =
+ Document_Output.document_output
+ {markdown = true, markup = fn body => [XML.Elem (Markup.latex_body name, body)]}
+ (NONE, Input.string (To_string0 s))
+
fun ml top (SML ml) = #generic_theory top
(ML_Context.exec let val source = input_source ml in
fn () => ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source
@@ -639,18 +644,27 @@ fun semi__theory (top : ('transitionM, 'transitionM, 'state) toplevel) = let ope
| Theory_axiomatization axiomatization =>
cons (\<^command_keyword>\<open>axiomatization\<close>, Cmd.axiomatization top axiomatization)
| Theory_section (Section (n, s)) => let val n = To_nat n in fn st => st
- |>:: (case n of 0 =>
+ |>:: let val (name, pos) = case n of 0 =>
\<^command_keyword>\<open>section\<close> | 1 =>
\<^command_keyword>\<open>subsection\<close> | _ =>
- \<^command_keyword>\<open>subsubsection\<close>,
- #tr_raw top (Pure_Syn.document_command {markdown = false} (NONE, Input.string (To_string0 s))))
+ \<^command_keyword>\<open>subsubsection\<close>
+ in
+ ( (name, pos)
+ , #tr_raw
+ top
+ (Document_Output.document_output
+ {markdown = false, markup = fn body => [XML.Elem (Markup.latex_heading name, body)]}
+ (NONE, Input.string (To_string0 s))))
+ end
|>:: (\<^command_keyword>\<open>print_syntax\<close>, #keep top (Cmd.section n s)) end
| Theory_text (Text s) =>
- cons (\<^command_keyword>\<open>text\<close>,
- #tr_raw top (Pure_Syn.document_command {markdown = true} (NONE, Input.string (To_string0 s))))
+ cons let val (name, pos) =
+ \<^command_keyword>\<open>text\<close>
+ in ((name, pos), #tr_raw top (Cmd.text name s)) end
| Theory_text_raw (Text_raw s) =>
- cons (\<^command_keyword>\<open>text_raw\<close>,
- #tr_raw top (Pure_Syn.document_command {markdown = true} (NONE, Input.string (To_string0 s))))
+ cons let val (name, pos) =
+ \<^command_keyword>\<open>text_raw\<close>
+ in ((name, pos), #tr_raw top (Cmd.text name s)) end
| Theory_ML ml =>
cons (\<^command_keyword>\<open>ML\<close>, Cmd.ml top ml)
| Theory_setup setup =>
@@ -747,7 +761,6 @@ structure Meta_Cmd_Data = Theory_Data
(open META
type T = T
val empty = []
- val extend = I
val merge = #2)
fun ML_context_exec pos ants =
@@ -763,7 +776,7 @@ fun meta_command0 s_put f_get constraint source =
Context.Theory
#> ML_context_exec (Input.pos_of source)
(ML_Lex.read "let open META val ML = META.SML val "
- @ ML_Lex.read_set_range (Input.range_of source) name
+ @ ML_Lex.read_range (Input.range_of source) name
@ ML_Lex.read (" : " ^ constraint ^ " = ")
@ ML_Lex.read_source source
@ ML_Lex.read (" in Context.>> (Context.map_theory (" ^ s_put ^ " " ^ name ^ ")) end"))
@@ -944,7 +957,6 @@ type T = (unit META.compiler_env_config_ext, theory) generation_mode
structure Data_gen = Theory_Data
(type T = T
val empty = {deep = [], shallow = [], syntax_print = [NONE]}
- val extend = I
fun merge (e1, e2) = { deep = #deep e1 @ #deep e2
, shallow = #shallow e1 @ #shallow e2
, syntax_print = #syntax_print e1 @ #syntax_print e2 })
@@ -1053,7 +1065,7 @@ fun meta_command0 s_put f_get f_get0 constraint source =
Context.Theory
#> Bind_META.ML_context_exec (Input.pos_of source)
(ML_Lex.read "let open META val ML = META.SML val "
- @ ML_Lex.read_set_range (Input.range_of source) name
+ @ ML_Lex.read_range (Input.range_of source) name
@ ML_Lex.read (" : " ^ constraint ^ " = ")
@ ML_Lex.read_source source
@ ML_Lex.read (" in Context.>> (Context.map_theory (fn thy => " ^ s_put ^ " (" ^ name ^ " (" ^ f_get0 ^ " thy)) thy)) end"))
diff --git a/Citadelle/src/compiler_misc/Aux_text.thy b/Citadelle/src/compiler_misc/Aux_text.thy
index 4ff7b6b50ef..0d4d9e35b4d 100644
--- a/Citadelle/src/compiler_misc/Aux_text.thy
+++ b/Citadelle/src/compiler_misc/Aux_text.thy
@@ -54,7 +54,6 @@ datatype code_printing = Code_printing of string * Position.T
structure Data_code = Theory_Data
(type T = code_printing list Symtab.table
val empty = Symtab.empty
- val extend = I
val merge = Symtab.merge (K true))
val code_empty = ""
diff --git a/Citadelle/src/compiler_misc/meta/Printer_init.thy b/Citadelle/src/compiler_misc/meta/Printer_init.thy
index a3286a211da..863947a3fe8 100644
--- a/Citadelle/src/compiler_misc/meta/Printer_init.thy
+++ b/Citadelle/src/compiler_misc/meta/Printer_init.thy
@@ -229,7 +229,6 @@ datatype code_printing = Code_printing of
structure Data_code = Theory_Data
(type T = code_printing list Symtab.table
val empty = Symtab.empty
- val extend = I
val merge = Symtab.merge (K true))
val code_empty = ""
diff --git a/Citadelle/src/uml_main/UML_PropertyProfiles.thy b/Citadelle/src/uml_main/UML_PropertyProfiles.thy
index 6e4059c9412..8ddcc9c1601 100644
--- a/Citadelle/src/uml_main/UML_PropertyProfiles.thy
+++ b/Citadelle/src/uml_main/UML_PropertyProfiles.thy
@@ -317,7 +317,7 @@ sublocale profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^
apply(simp)
apply(subst cp_valid, simp)
apply (simp add: const_valid)
- apply (metis (hide_lams, mono_tags) OclValid_def def_scheme defined5 defined6 defined_and_I foundation1 foundation10' foundation16' foundation18 foundation21 foundation22 foundation9)
+ apply (metis (opaque_lifting, mono_tags) OclValid_def def_scheme defined5 defined6 defined_and_I foundation1 foundation10' foundation16' foundation18 foundation21 foundation22 foundation9)
apply(simp add: def_scheme, subst StrongEq_def, simp)
by (metis OclValid_def def_scheme defined7 foundation16)
@@ -371,7 +371,7 @@ locale profile_bin\<^sub>v_\<^sub>v =
sublocale profile_bin\<^sub>v_\<^sub>v < profile_bin_scheme valid valid
apply(unfold_locales)
apply(simp, subst cp_valid, simp, rule const_valid, simp)+
- apply (metis (hide_lams, mono_tags) OclValid_def def_scheme defined5 defined6 defined_and_I
+ apply (metis (opaque_lifting, mono_tags) OclValid_def def_scheme defined5 defined6 defined_and_I
foundation1 foundation10' foundation16' foundation18 foundation21 foundation22 foundation9)
apply(simp add: def_scheme)
apply(simp add: defined_def OclValid_def false_def true_def
diff --git a/Citadelle/src/uml_main/UML_State.thy b/Citadelle/src/uml_main/UML_State.thy
index 4029ae19b91..430ec3e962e 100644
--- a/Citadelle/src/uml_main/UML_State.thy
+++ b/Citadelle/src/uml_main/UML_State.thy
@@ -937,12 +937,12 @@ theorem framing:
apply(simp add: UML_Set.OclExcluding_def split: if_split_asm)
apply(subst (asm) (2) Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse)
apply(simp, (rule disjI2)+)
- apply (metis (hide_lams, mono_tags) Diff_iff Set_inv_lemma def_X)
+ apply (metis (opaque_lifting, mono_tags) Diff_iff Set_inv_lemma def_X)
apply(simp)
apply(erule ballE[where P = "\<lambda>x. x \<noteq> null"]) apply(assumption)
apply(simp)
- apply (metis (hide_lams, no_types) def_x foundation16[THEN iffD1])
- apply (metis (hide_lams, no_types) OclValid_def def_X def_x foundation20
+ apply (metis (opaque_lifting, no_types) def_x foundation16[THEN iffD1])
+ apply (metis (opaque_lifting, no_types) OclValid_def def_X def_x foundation20
OclExcluding_valid_args_valid OclExcluding_valid_args_valid'')
by(simp add: invalid_def bot_option_def)
@@ -960,11 +960,11 @@ theorem framing:
apply(drule foundation5[simplified OclValid_def true_def], simp)
apply(subst (asm) Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e_inverse, simp)
apply(rule disjI2)+
- apply (metis (hide_lams, no_types) DiffD1 OclValid_def Set_inv_lemma def_x
+ apply (metis (opaque_lifting, no_types) DiffD1 OclValid_def Set_inv_lemma def_x
foundation16 foundation18')
apply(simp)
apply(erule_tac x = "oid_of (x (\<sigma>, \<sigma>'))" in ballE) apply simp+
- apply (metis (hide_lams, no_types)
+ apply (metis (opaque_lifting, no_types)
DiffD1 image_iff image_insert insert_Diff_single insert_absorb oid_is_typerepr)
apply(simp add: invalid_def bot_option_def)+
by blast
@@ -1126,7 +1126,7 @@ lemma fold_val_elem\<^sub>S\<^sub>e\<^sub>q:
shows "list_all (\<lambda>x. (\<tau> \<Turnstile> \<upsilon> (f p x))) s_set"
apply(rule rev_induct[where P = "\<lambda>s_set. \<tau> \<Turnstile> \<upsilon> foldl UML_Sequence.OclIncluding Sequence{} (List.map (f p) s_set) \<longrightarrow> list_all (\<lambda>x. \<tau> \<Turnstile> \<upsilon> f p x) s_set", THEN mp])
apply(simp, auto)
- apply (metis (hide_lams, mono_tags) UML_Sequence.OclIncluding.def_valid_then_def UML_Sequence.OclIncluding.defined_args_valid foundation20)+
+ apply (metis (opaque_lifting, mono_tags) UML_Sequence.OclIncluding.def_valid_then_def UML_Sequence.OclIncluding.defined_args_valid foundation20)+
by(simp add: assms)
lemma fold_val_elem\<^sub>S\<^sub>e\<^sub>t:
@@ -1134,7 +1134,7 @@ lemma fold_val_elem\<^sub>S\<^sub>e\<^sub>t:
shows "list_all (\<lambda>x. (\<tau> \<Turnstile> \<upsilon> (f p x))) s_set"
apply(rule rev_induct[where P = "\<lambda>s_set. \<tau> \<Turnstile> \<upsilon> foldl UML_Set.OclIncluding Set{} (List.map (f p) s_set) \<longrightarrow> list_all (\<lambda>x. \<tau> \<Turnstile> \<upsilon> f p x) s_set", THEN mp])
apply(simp, auto)
- apply (metis (hide_lams, mono_tags) foundation10' foundation20)+
+ apply (metis (opaque_lifting, mono_tags) foundation10' foundation20)+
by(simp add: assms)
lemma select_object_any_defined0\<^sub>S\<^sub>e\<^sub>q:
@@ -1346,7 +1346,7 @@ proof -
proof - fix z' a list show "(\<lambda>x. f x \<tau>) ` set s_set = {z'} \<Longrightarrow> s_set = a # list \<Longrightarrow> \<exists>e. List.member s_set e \<and> z' = f e \<tau>"
apply(drule list_same[where x1 = a])
apply (metis member_rec(1))
- by (metis (hide_lams, mono_tags) ListMem_iff elem in_set_member)
+ by (metis (opaque_lifting, mono_tags) ListMem_iff elem in_set_member)
qed
qed blast+
--
GitLab