diff -r 8927b737936f -r 925232418a15 thys/Positions.thy
--- a/thys/Positions.thy	Mon Jun 26 18:40:58 2017 +0100
+++ b/thys/Positions.thy	Tue Jun 27 01:02:17 2017 +0100
@@ -21,13 +21,11 @@
 | "Pos (Right v) = {[]} \<union> {1#ps | ps. ps \<in> Pos v}"
 | "Pos (Seq v1 v2) = {[]} \<union> {0#ps | ps. ps \<in> Pos v1} \<union> {1#ps | ps. ps \<in> Pos v2}" 
 | "Pos (Stars []) = {[]}"
-| "Pos (Stars (v#vs)) = {[]} \<union> {0#ps | ps. ps \<in> Pos v} \<union> {(Suc n)#ps | n ps. n#ps \<in> Pos (Stars vs)}"
+| "Pos (Stars (v#vs)) = {[]} \<union> {0#ps | ps. ps \<in> Pos v} \<union> {Suc n#ps | n ps. n#ps \<in> Pos (Stars vs)}"
 
 lemma Pos_empty:
   shows "[] \<in> Pos v"
-apply(induct v rule: Pos.induct)
-apply(auto)
-done
+by (induct v rule: Pos.induct)(auto)
 
 fun intlen :: "'a list \<Rightarrow> int"
 where
@@ -36,15 +34,11 @@
 
 lemma inlen_bigger:
   shows "0 \<le> intlen xs"
-apply(induct xs)
-apply(auto)
-done 
+by (induct xs)(auto)
 
 lemma intlen_append:
   shows "intlen (xs @ ys) = intlen xs + intlen ys"
-apply(induct xs arbitrary: ys)
-apply(auto)
-done 
+by (induct xs arbitrary: ys) (auto)
 
 lemma intlen_length:
   assumes "length xs < length ys"
@@ -69,29 +63,17 @@
   and   "pflat_len (Left v) (Suc 0#p) = -1"
   and   "pflat_len (Right v) (Suc 0#p) = pflat_len v p"
   and   "pflat_len (Right v) (0#p) = -1"
+  and   "pflat_len (Stars (v#vs)) (Suc n#p) = pflat_len (Stars vs) (n#p)"
+  and   "pflat_len (Stars (v#vs)) (0#p) = pflat_len v p"
   and   "pflat_len v [] = intlen (flat v)"
-apply(auto simp add: pflat_len_def Pos_empty)
-done
+by (auto simp add: pflat_len_def Pos_empty)
 
 lemma pflat_len_Stars_simps:
   assumes "n < length vs"
   shows "pflat_len (Stars vs) (n#p) = pflat_len (vs!n) p"
 using assms 
 apply(induct vs arbitrary: n p)
-apply(simp)
-apply(simp)
-apply(simp add: pflat_len_def)
-apply(auto)[1]
-apply (metis at.simps(6))
-apply (metis Suc_less_eq Suc_pred)
-by (metis diff_Suc_1 less_Suc_eq_0_disj nth_Cons')
-
-
-lemma pflat_len_Stars_simps2:
-  shows "pflat_len (Stars (v#vs)) (Suc n # p) = pflat_len (Stars vs) (n#p)"
-  and   "pflat_len (Stars (v#vs)) (0 # p) = pflat_len v p"
-using assms 
-apply(simp_all add: pflat_len_def)
+apply(auto simp add: less_Suc_eq_0_disj pflat_len_simps)
 done
 
 lemma Two_to_Three_aux:
@@ -103,7 +85,6 @@
 apply (smt inlen_bigger)+
 done
 
-
 lemma Two_to_Three_orig:
   assumes "\<forall>p \<in> Pos v1 \<union> Pos v2. pflat_len v1 p = pflat_len v2 p"
   shows "Pos v1 = Pos v2"
@@ -308,7 +289,7 @@
 where
   "ps1 \<sqsubset>spre ps2 \<equiv> (ps1 \<sqsubseteq>pre ps2 \<and> ps1 \<noteq> ps2)"
 
-inductive lex_lists :: "nat list \<Rightarrow> nat list \<Rightarrow> bool" ("_ \<sqsubset>lex _")
+inductive lex_list :: "nat list \<Rightarrow> nat list \<Rightarrow> bool" ("_ \<sqsubset>lex _")
 where
   "[] \<sqsubset>lex p#ps"
 | "ps1 \<sqsubset>lex ps2 \<Longrightarrow> (p#ps1) \<sqsubset>lex (p#ps2)"
@@ -319,71 +300,36 @@
   assumes "ps1 \<sqsubset>lex ps2"
   shows "ps1 \<noteq> ps2"
 using assms
-apply(induct rule: lex_lists.induct)
+apply(induct rule: lex_list.induct)
 apply(auto)
 done
 
-lemma lex_append:
-  assumes "ps2 \<noteq> []"  
-  shows "ps \<sqsubset>lex ps @ ps2"
-using assms
-apply(induct ps)
-apply(auto intro: lex_lists.intros)
-apply(case_tac ps2)
-apply(simp)
-apply(simp)
-apply(auto intro: lex_lists.intros)
-done
-
-lemma lexordp_simps [simp]:
+lemma lex_simps [simp]:
   fixes xs ys :: "nat list"
-  shows "[] \<sqsubset>lex ys = (ys \<noteq> [])"
-  and   "xs \<sqsubset>lex [] = False"
+  shows "[] \<sqsubset>lex ys \<longleftrightarrow> ys \<noteq> []"
+  and   "xs \<sqsubset>lex [] \<longleftrightarrow> False"
   and   "(x # xs) \<sqsubset>lex (y # ys) \<longleftrightarrow> (x < y \<or> (\<not> y < x \<and> xs \<sqsubset>lex ys))"
 apply -
-apply (metis lex_append lex_lists.simps list.simps(3))
-using lex_lists.cases apply blast
-using lex_lists.cases lex_lists.intros(2) lex_lists.intros(3) not_less_iff_gr_or_eq by fastforce
+apply (metis lex_irrfl lex_list.intros(1) list.exhaust)
+using lex_list.cases apply blast
+using lex_list.cases lex_list.intros(2) lex_list.intros(3) not_less_iff_gr_or_eq by fastforce
 
-lemma lex_append_cancel [simp]:
-  fixes ps ps1 ps2 :: "nat list"
-  shows "ps @ ps1 \<sqsubset>lex ps @ ps2 \<longleftrightarrow> ps1 \<sqsubset>lex ps2"
-apply(induct ps)
-apply(auto)
-done
 
 lemma lex_trans:
   fixes ps1 ps2 ps3 :: "nat list"
   assumes "ps1 \<sqsubset>lex ps2" "ps2 \<sqsubset>lex ps3"
   shows "ps1 \<sqsubset>lex ps3"
 using assms
-apply(induct arbitrary: ps3 rule: lex_lists.induct)
-apply(erule lex_lists.cases)
+apply(induct arbitrary: ps3 rule: lex_list.induct)
+apply(erule lex_list.cases)
 apply(simp_all)
 apply(rotate_tac 2)
-apply(erule lex_lists.cases)
+apply(erule lex_list.cases)
 apply(simp_all)
-apply(erule lex_lists.cases)
+apply(erule lex_list.cases)
 apply(simp_all)
 done
 
-lemma trichotomous_aux:
-  fixes p q :: "nat list"
-  assumes "p \<sqsubset>lex q" "p \<noteq> q"
-  shows "\<not>(q \<sqsubset>lex p)"
-using assms
-apply(induct rule: lex_lists.induct)
-apply(auto)
-done
-
-lemma trichotomous_aux2:
-  fixes p q :: "nat list"
-  assumes "p \<sqsubset>lex q" "q \<sqsubset>lex p"
-  shows "False"
-using assms
-apply(induct rule: lex_lists.induct)
-apply(auto)
-done
 
 lemma trichotomous:
   fixes p q :: "nat list"
@@ -394,12 +340,6 @@
 apply(auto)
 done
 
-(*
-definition dpos :: "val \<Rightarrow> val \<Rightarrow> nat list \<Rightarrow> bool" 
-  where
-  "dpos v1 v2 p \<equiv> (p \<in> Pos v1 \<union> Pos v2) \<and> (p \<notin> Pos v1 \<inter> Pos v2)"
-*)
-
 lemma outside_lemma:
   assumes "p \<notin> Pos v1 \<union> Pos v2"
   shows "pflat_len v1 p = pflat_len v2 p"
@@ -407,35 +347,6 @@
 apply(auto simp add: pflat_len_def)
 done
 
-(*
-lemma dpos_lemma_aux:
-  assumes "p \<in> Pos v1 \<union> Pos v2"
-  and "pflat_len v1 p = pflat_len v2 p"
-  shows "p \<in> Pos v1 \<inter> Pos v2"
-using assms
-apply(auto simp add: pflat_len_def)
-apply (smt inlen_bigger)
-apply (smt inlen_bigger)
-done
-
-lemma dpos_lemma:
-  assumes "p \<in> Pos v1 \<union> Pos v2"
-  and "pflat_len v1 p = pflat_len v2 p"
-  shows "\<not>dpos v1 v2 p"
-using assms
-apply(auto simp add: dpos_def dpos_lemma_aux)
-using dpos_lemma_aux apply auto[1]
-using dpos_lemma_aux apply auto[1]
-done
-
-lemma dpos_lemma2:
-  assumes "p \<in> Pos v1 \<union> Pos v2"
-  and "dpos v1 v2 p"
-  shows "pflat_len v1 p \<noteq> pflat_len v2 p"
-using assms
-using dpos_lemma by blast
-*)
-
 definition val_ord:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _")
 where
   "v1 \<sqsubset>val p v2 \<equiv> (p \<in> Pos v1 \<and> pflat_len v1 p > pflat_len v2 p \<and>
@@ -453,78 +364,48 @@
 lemma val_ord_shorterI:
   assumes "length (flat v') < length (flat v)"
   shows "v :\<sqsubset>val v'" 
-using assms(1)
-apply(subst val_ord_ex_def)
-apply(rule_tac x="[]" in exI)
-apply(subst val_ord_def)
-apply(rule conjI)
-apply (simp add: Pos_empty)
-apply(rule conjI)
-apply(simp add: pflat_len_simps)
-apply (simp add: intlen_length)
-apply(simp)
-done
+using assms
+unfolding val_ord_ex_def
+by (metis Pos_empty intlen_length lex_simps(2) pflat_len_simps(9) val_ord_def)
 
-lemma val_ord_spre:
+lemma val_ord_spreI:
   assumes "(flat v') \<sqsubset>spre (flat v)"
   shows "v :\<sqsubset>val v'" 
-using assms(1)
+using assms
 apply(rule_tac val_ord_shorterI)
-apply(simp add: sprefix_list_def prefix_list_def)
-apply(auto)
-apply(case_tac ps')
-apply(auto)
-by (metis append_eq_conv_conj drop_all le_less_linear neq_Nil_conv)
+by (metis append_eq_conv_conj le_less_linear prefix_list_def sprefix_list_def take_all)
 
-
-lemma val_ord_ALTI:
-  assumes "v \<sqsubset>val p v'" "flat v = flat v'"
-  shows "(Left v) \<sqsubset>val (0#p) (Left v')" 
+lemma val_ord_LeftI:
+  assumes "v :\<sqsubset>val v'" "flat v = flat v'"
+  shows "(Left v) :\<sqsubset>val (Left v')" 
 using assms(1)
-apply(subst (asm) val_ord_def)
-apply(erule conjE)
-apply(subst val_ord_def)
-apply(rule conjI)
-apply(simp)
-apply(rule conjI)
-apply(simp add: pflat_len_simps)
-apply(rule ballI)
-apply(rule impI)
-apply(simp only: Pos.simps)
-apply(auto)[1]
+unfolding val_ord_ex_def
+apply(auto)
+apply(rule_tac x="0#p" in exI)
 using assms(2)
-apply(simp add: pflat_len_simps)
-apply(auto simp add: pflat_len_simps)[2]
+apply(auto simp add: val_ord_def pflat_len_simps)
 done
 
-lemma val_ord_ALTI2:
-  assumes "v \<sqsubset>val p v'" "flat v = flat v'"
-  shows "(Right v) \<sqsubset>val (1#p) (Right v')" 
+lemma val_ord_RightI:
+  assumes "v :\<sqsubset>val v'" "flat v = flat v'"
+  shows "(Right v) :\<sqsubset>val (Right v')" 
 using assms(1)
-apply(subst (asm) val_ord_def)
-apply(erule conjE)
-apply(subst val_ord_def)
-apply(rule conjI)
-apply(simp)
-apply(rule conjI)
-apply(simp add: pflat_len_simps)
-apply(rule ballI)
-apply(rule impI)
-apply(simp only: Pos.simps)
-apply(auto)[1]
+unfolding val_ord_ex_def
+apply(auto)
+apply(rule_tac x="Suc 0#p" in exI)
 using assms(2)
-apply(simp add: pflat_len_simps)
-apply(auto simp add: pflat_len_simps)[2]
+apply(auto simp add: val_ord_def pflat_len_simps)
 done
 
+
 lemma val_ord_ALTE:
   assumes "(Left v1) \<sqsubset>val (p # ps) (Left v2)"
   shows "p = 0 \<and> v1 \<sqsubset>val ps v2"
 using assms(1)
 apply(simp add: val_ord_def)
 apply(auto simp add: pflat_len_simps)
-apply (metis (no_types, hide_lams) assms lex_lists.intros(2) outside_lemma pflat_len_simps(3) val_ord_def)
-by (metis (no_types, hide_lams) assms lex_lists.intros(2) outside_lemma pflat_len_simps(3) val_ord_def)
+apply (metis (no_types, hide_lams) assms lex_list.intros(2) outside_lemma pflat_len_simps(3) val_ord_def)
+by (metis (no_types, hide_lams) assms lex_list.intros(2) outside_lemma pflat_len_simps(3) val_ord_def)
 
 lemma val_ord_ALTE2:
   assumes "(Right v1) \<sqsubset>val (p # ps) (Right v2)"
@@ -532,8 +413,8 @@
 using assms(1)
 apply(simp add: val_ord_def)
 apply(auto simp add: pflat_len_simps)
-apply (metis (no_types, hide_lams) assms lex_lists.intros(2) outside_lemma pflat_len_simps(5) val_ord_def)
-by (metis (no_types, hide_lams) assms lex_lists.intros(2) outside_lemma pflat_len_simps(5) val_ord_def)
+apply (metis (no_types, hide_lams) assms lex_list.intros(2) outside_lemma pflat_len_simps(5) val_ord_def)
+by (metis (no_types, hide_lams) assms lex_list.intros(2) outside_lemma pflat_len_simps(5) val_ord_def)
 
 lemma val_ord_STARI:
   assumes "v1 \<sqsubset>val p v2" "flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))"
@@ -585,7 +466,7 @@
 apply(simp)
 using assms(2)
 apply(auto)
-apply (simp add: pflat_len_simps(7))
+apply (simp add: pflat_len_simps(9))
 apply (simp add: pflat_len_Stars_simps)
 using assms(2)
 apply(auto simp add: pflat_len_def)[1]
@@ -795,39 +676,6 @@
 by (metis IntE Two_to_Three_aux UnCI lex_trans outside_lemma)
 
 
-lemma Pos_pre:
-  assumes "p \<in> Pos v" "q \<sqsubseteq>pre p"
-  shows "q \<in> Pos v"
-using assms
-apply(induct v arbitrary: p q rule: Pos.induct)
-apply(simp_all add: prefix_list_def)
-apply (meson append_eq_Cons_conv append_is_Nil_conv)
-apply (meson append_eq_Cons_conv append_is_Nil_conv)
-apply (metis (no_types, lifting) Cons_eq_append_conv append_is_Nil_conv)
-apply(auto)
-apply (meson append_eq_Cons_conv)
-apply(simp add: append_eq_Cons_conv)
-apply(auto)
-done
-
-lemma lex_lists_order:
-  assumes "q' \<sqsubset>lex q" "\<not>(q' \<sqsubseteq>pre q)"
-  shows "\<not>(q \<sqsubset>lex q')"
-using assms
-apply(induct rule: lex_lists.induct)
-apply(simp add: prefix_list_def)
-apply(auto)
-using trichotomous_aux2 by auto
-
-lemma lex_appendL:
-  assumes "q \<sqsubset>lex p" 
-  shows "q \<sqsubset>lex p @ q'"
-using assms
-apply(induct arbitrary: q' rule: lex_lists.induct)
-apply(auto)
-done
-
-
 inductive 
   CPrf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)
 where
@@ -943,17 +791,6 @@
 apply(simp_all)[7]
 done
 
-lemma CPTpre_SEQ:
-  assumes "v \<in> CPTpre (SEQ r1 r2) s"
-  shows "\<exists>s'. flat v = s' \<and> (s' \<sqsubseteq>pre s) \<and> s' \<in> L (SEQ r1 r2)"
-using assms
-apply(simp add: CPTpre_simps)
-apply(auto simp add: CPTpre_def)
-apply (simp add: prefix_list_def)
-by (metis L.simps(4) L_flat_Prf1 Prf.intros(1) Prf_CPrf flat.simps(5))
-
-term "{vs. Stars vs \<in> A}"
-
 lemma test: 
   assumes "finite A"
   shows "finite {vs. Stars vs \<in> A}"
@@ -1138,10 +975,9 @@
 apply(erule exE)
 apply(subst val_ord_ex1_def)
 apply(rule disjI1)
+apply(rule val_ord_LeftI)
 apply(subst val_ord_ex_def)
-apply(rule_tac x="0#p" in exI)
-apply(rule val_ord_ALTI)
-apply(simp)
+apply(auto)[1]
 using Posix1(2) apply blast
 using val_ord_ex1_def apply blast
 apply(subst val_ord_ex1_def)
@@ -1192,13 +1028,9 @@
 apply(auto simp add: CPTpre_def)[1]
 apply(subst (asm) val_ord_ex1_def)
 apply(erule disjE)
-apply(subst (asm) val_ord_ex_def)
-apply(erule exE)
 apply(subst val_ord_ex1_def)
 apply(rule disjI1)
-apply(subst val_ord_ex_def)
-apply(rule_tac x="1#p" in exI)
-apply(rule val_ord_ALTI2)
+apply(rule val_ord_RightI)
 apply(simp)
 using Posix1(2) apply blast
 apply (simp add: val_ord_ex1_def)
@@ -1253,7 +1085,10 @@
 apply (subst val_ord_ex_def)
 apply(case_tac p)
 apply(simp)
-apply (metis Posix1(2) flat_Stars not_less_iff_gr_or_eq pflat_len_simps(7) same_append_eq val_ord_def)
+apply (metis Posix1(2) append_eq_conv_conj flat_Stars not_less_iff_gr_or_eq pflat_len_simps(9) val_ord_def)
+
+
+
 using Posix1(2) val_ord_STARI2 apply fastforce
 apply(simp add: val_ord_ex1_def)
 apply (subst (asm) val_ord_ex_def)
@@ -1283,13 +1118,13 @@
 apply(simp add: val_ord_def)
 apply(rule conjI)
 apply(simp add: val_ord_def)
-apply(auto simp add: pflat_len_simps pflat_len_Stars_simps2)[1]
+apply(auto simp add: pflat_len_simps)[1]
 apply(rule ballI)
 apply(rule impI)
-apply(simp add: val_ord_def pflat_len_simps pflat_len_Stars_simps2 intlen_append)
+apply(simp add: val_ord_def pflat_len_simps intlen_append)
 apply(clarify)
 apply(case_tac q)
-apply(simp add: val_ord_def pflat_len_simps pflat_len_Stars_simps2 intlen_append)
+apply(simp add: val_ord_def pflat_len_simps intlen_append)
 apply(clarify)
 apply(erule disjE)
 prefer 2
@@ -1297,12 +1132,12 @@
 apply(simp)
 apply(drule mp)
 apply(simp)
-apply(simp add: val_ord_def pflat_len_simps pflat_len_Stars_simps2 intlen_append)
+apply(simp add: val_ord_def pflat_len_simps intlen_append)
 apply(drule_tac x="Suc a # list" in bspec)
 apply(simp)
 apply(drule mp)
 apply(simp)
-apply(simp add: val_ord_def pflat_len_simps pflat_len_Stars_simps2 intlen_append)
+apply(simp add: val_ord_def pflat_len_simps intlen_append)
 done
 
 
@@ -1313,14 +1148,6 @@
 by (metis Posix_val_ord_stronger less_irrefl val_ord_def 
     val_ord_ex1_def val_ord_ex_def val_ord_ex_trans)
 
-thm Posix.intros(6)
-
-inductive Prop :: "rexp \<Rightarrow> val list \<Rightarrow> bool"
-where
-  "Prop r []"
-| "\<lbrakk>Prop r vs; 
-    \<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = concat (map flat vs) \<and> flat v @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk> 
-   \<Longrightarrow> Prop r (v # vs)"
 
 lemma STAR_val_ord_ex:
   assumes "Stars (v # vs1) :\<sqsubset>val Stars (v # vs2)"
@@ -1339,7 +1166,7 @@
 apply(clarify)
 prefer 2
 using STAR_val_ord val_ord_ex_def apply blast
-apply(auto simp add: pflat_len_Stars_simps2 val_ord_def pflat_len_def)[1]
+apply(auto simp add: pflat_len_simps val_ord_def pflat_len_def)[1]
 done
 
 lemma STAR_val_ord_exI:
@@ -1384,25 +1211,6 @@
 apply(auto)
 done
 
-lemma Posix_STARI:
-  assumes "\<forall>v \<in> set vs. flat v \<noteq> [] \<and> (flat v) \<in> r \<rightarrow> v" "Prop r vs"
-  shows "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs"
-using assms
-apply(induct vs arbitrary: r)
-apply(simp)
-apply(rule Posix.intros)
-apply(simp)
-apply(rule Posix.intros)
-apply(simp)
-apply(auto)[1]
-apply(erule Prop.cases)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(erule Prop.cases)
-apply(simp)
-apply(auto)[1]
-done
 
 lemma CPrf_stars:
   assumes "\<Turnstile> Stars vs : STAR r"
@@ -1462,7 +1270,7 @@
 apply (meson CPrf_stars Prf.intros(7) Prf_CPrf list.set_intros(1))
 apply(subst (asm) (2) val_ord_ex_def)
 apply(simp)
-apply (metis flat.simps(7) flat_Stars intlen.cases not_less_iff_gr_or_eq pflat_len_simps(7) val_ord_STARI2 val_ord_def val_ord_ex_def)
+apply (metis flat.simps(7) flat_Stars intlen.cases not_less_iff_gr_or_eq pflat_len_simps(9) val_ord_STARI2 val_ord_def val_ord_ex_def)
 apply(auto simp add: CPT_def PT_def)[1]
 using CPrf_stars apply auto[1]
 apply(auto)[1]
@@ -1502,7 +1310,7 @@
 apply(simp)
 apply(subst (asm) (2) val_ord_ex_def)
 apply(simp)
-apply (metis flat.simps(7) flat_Stars intlen.cases not_less_iff_gr_or_eq pflat_len_simps(7) val_ord_STARI2 val_ord_def val_ord_ex_def)
+apply (metis flat.simps(7) flat_Stars intlen.cases not_less_iff_gr_or_eq pflat_len_simps(9) val_ord_STARI2 val_ord_def val_ord_ex_def)
 proof -
   fix a :: val and vsa :: "val list" and s\<^sub>3 :: "char list" and vA :: val and vB :: "val list"
   assume a1: "s\<^sub>3 \<noteq> []"
@@ -1576,7 +1384,7 @@
 apply(drule mp)
 apply(rule Prf.intros)
 apply(simp)
-apply (meson val_ord_ALTI val_ord_ex_def)
+apply (meson val_ord_LeftI)
 apply(assumption)
 (* ALT Right *)
 apply(auto simp add: CPT_def)[1]
@@ -1593,9 +1401,7 @@
 apply(drule mp)
 apply(rule Prf.intros)
 apply(simp)
-apply(subst (asm) (2) val_ord_ex_def)
-apply(erule exE)
-apply(drule val_ord_ALTI2)
+apply(drule val_ord_RightI)
 apply(assumption)
 apply(auto simp add: val_ord_ex_def)[1]
 apply(assumption)