Mercurial Mercurial > hg > lexing / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
almost there
authorChengsong
Fri, 15 Apr 2022 23:31:31 +0100
changeset 490 64183736777a
parent 489 2b5b3f83e2b6
child 491 48ce16d61e03
almost there
thys2/ClosedForms.thy file | annotate | diff | comparison | revisions 
--- a/thys2/ClosedForms.thy	Fri Apr 15 19:35:29 2022 +0100
+++ b/thys2/ClosedForms.thy	Fri Apr 15 23:31:31 2022 +0100
@@ -8,13 +8,21 @@
   apply simp
   by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
 
-lemma simp_flatten3:
-  shows "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))"
-  apply(induct rsa)
+
+
+lemma simp_flatten_aux0:
+  shows "rsimp (RALTS rs) = rsimp (RALTS (map rsimp rs))"
+  by (metis append_Nil head_one_more_simp identity_wwo0 list.simps(8) rdistinct.simps(1) rflts.simps(1) rsimp.simps(2) rsimp_ALTs.simps(1) rsimp_ALTs.simps(3) simp_flatten spawn_simp_rsimpalts)
+
+
+
+
+
+
+
+
+
   
-  using simp_flatten apply force
-
-  sorry
 
 inductive 
   hrewrite:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99)
@@ -415,6 +423,216 @@
   by blast
 
 
+lemma good_singleton:
+  shows "good a \<and> nonalt a  \<Longrightarrow> rflts [a] = [a]"
+  using good.simps(1) k0b by blast
+
+
+
+
+
+
+
+lemma all_that_same_elem:
+  shows "\<lbrakk> a \<in> rset; rdistinct rs {a} = []\<rbrakk>
+       \<Longrightarrow> rdistinct (rs @ rsb) rset = rdistinct rsb rset"
+  apply(induct rs)
+   apply simp
+  apply(subgoal_tac "aa = a")
+   apply simp
+  by (metis empty_iff insert_iff list.discI rdistinct.simps(2))
+
+lemma distinct_early_app1:
+  shows "rset1 \<subseteq> rset \<Longrightarrow> rdistinct rs rset = rdistinct (rdistinct rs rset1) rset"
+  apply(induct rs arbitrary: rset rset1)
+   apply simp
+  apply simp
+  apply(case_tac "a \<in> rset1")
+   apply simp
+   apply(case_tac "a \<in> rset")
+    apply simp+
+  
+   apply blast
+  apply(case_tac "a \<in> rset1")
+   apply simp+
+  apply(case_tac "a \<in> rset")
+   apply simp
+   apply (metis insert_subsetI)
+  apply simp
+  by (meson insert_mono)
+
+
+lemma distinct_early_app:
+  shows " rdistinct (rs @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset"
+  apply(induct rsb)
+   apply simp
+  using distinct_early_app1 apply blast
+  by (metis distinct_early_app1 distinct_once_enough empty_subsetI)
+
+
+lemma distinct_eq_interesting1:
+  shows "a \<in> rset \<Longrightarrow> rdistinct (rs @ rsb) rset = rdistinct (rdistinct (a # rs) {} @ rsb) rset"
+  apply(subgoal_tac "rdistinct (rdistinct (a # rs) {} @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset")
+   apply(simp only:)
+  using distinct_early_app apply blast 
+  by (metis append_Cons distinct_early_app rdistinct.simps(2))
+
+
+
+lemma good_flatten_aux_aux1:
+  shows "\<lbrakk> size rs \<ge>2; 
+\<forall>r \<in> set rs. good r \<and> r \<noteq> RZERO \<and> nonalt r; \<forall>r \<in> set rsb. good r \<and> r \<noteq> RZERO \<and> nonalt r \<rbrakk>
+       \<Longrightarrow> rdistinct (rs @ rsb) rset =
+           rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset"
+  apply(induct rs arbitrary: rset)
+   apply simp
+  apply(case_tac "a \<in> rset")
+   apply simp
+   apply(case_tac "rdistinct rs {a}")
+    apply simp
+    apply(subst good_singleton)
+     apply force
+  apply simp
+    apply (meson all_that_same_elem)
+   apply(subgoal_tac "rflts [rsimp_ALTs (a # rdistinct rs {a})] = a # rdistinct rs {a} ")
+  prefer 2
+  using k0a rsimp_ALTs.simps(3) apply presburger
+  apply(simp only:)
+  apply(subgoal_tac "rdistinct (rs @ rsb) rset = rdistinct ((rdistinct (a # rs) {}) @ rsb) rset ")
+    apply (metis insert_absorb insert_is_Un insert_not_empty rdistinct.simps(2))
+   apply (meson distinct_eq_interesting1)
+  apply simp
+  apply(case_tac "rdistinct rs {a}")
+  prefer 2
+   apply(subgoal_tac "rsimp_ALTs (a # rdistinct rs {a}) = RALTS (a # rdistinct rs {a})")
+  apply(simp only:)
+  apply(subgoal_tac "a # rdistinct (rs @ rsb) (insert a rset) =
+           rdistinct (rflts [RALTS (a # rdistinct rs {a})] @ rsb) rset")
+   apply simp
+  apply (metis append_Cons distinct_early_app empty_iff insert_is_Un k0a rdistinct.simps(2))
+  using rsimp_ALTs.simps(3) apply presburger
+  by (metis Un_insert_left append_Cons distinct_early_app empty_iff good_singleton rdistinct.simps(2) rsimp_ALTs.simps(2) sup_bot_left)
+
+
+
+  
+
+lemma good_flatten_aux_aux:
+  shows "\<lbrakk>\<exists>a aa lista list. rs = a # list \<and> list = aa # lista; 
+\<forall>r \<in> set rs. good r \<and> r \<noteq> RZERO \<and> nonalt r; \<forall>r \<in> set rsb. good r \<and> r \<noteq> RZERO \<and> nonalt r \<rbrakk>
+       \<Longrightarrow> rdistinct (rs @ rsb) rset =
+           rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset"
+  apply(erule exE)+
+  apply(subgoal_tac "size rs \<ge> 2")
+   apply (metis good_flatten_aux_aux1)
+  by (simp add: Suc_leI length_Cons less_add_Suc1)
+
+
+
+lemma good_flatten_aux:
+  shows " \<lbrakk>\<forall>r\<in>set rs. good r; \<forall>r\<in>set rsa. good r; \<forall>r\<in>set rsb. good r;
+     rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (rsa @ rs @ rsb)) {});
+     rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) =
+     rsimp_ALTs (rdistinct (rflts (rsa @ [rsimp (RALTS rs)] @ rsb)) {});
+     map rsimp rsa = rsa; map rsimp rsb = rsb; map rsimp rs = rs;
+     rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} =
+     rdistinct (rflts rsa) {} @ rdistinct (rflts rs @ rflts rsb) (set (rflts rsa));
+     rdistinct (rflts rsa @ rflts [rsimp (RALTS rs)] @ rflts rsb) {} =
+     rdistinct (rflts rsa) {} @ rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))\<rbrakk>
+    \<Longrightarrow>    rdistinct (rflts rs @ rflts rsb) rset =
+           rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) rset"
+  apply simp
+  apply(case_tac "rflts rs ")
+   apply simp
+  apply(case_tac "list")
+   apply simp
+   apply(case_tac "a \<in> rset")
+    apply simp
+  apply (metis append_Cons append_Nil flts_append list.set(1) list.simps(15) nonalt.simps(1) nonalt0_flts_keeps nonalt_flts_rd qqq1 rdistinct.simps(2) rdistinct_set_equality singleton_iff)
+   apply simp
+  apply (metis Un_insert_left append_Cons append_Nil ex_in_conv flts_single1 insertI1 list.simps(15) nonalt_flts_rd nonazero.elims(3) qqq1 rdistinct.simps(2) sup_bot_left)
+  apply(subgoal_tac "\<forall>r \<in> set (rflts rs). good r \<and> r \<noteq> RZERO \<and> nonalt r")
+  prefer 2  
+  apply (metis flts3 nn1b nn1c qqq1 test)
+  apply(subgoal_tac "\<forall>r \<in> set (rflts rsb). good r \<and> r \<noteq> RZERO \<and> nonalt r")
+  prefer 2  
+  apply (metis flts3 nn1b nn1c qqq1 test)
+  by (smt (verit, ccfv_threshold) good_flatten_aux_aux)
+
+  
+
+
+lemma good_flatten_middle:
+  shows "\<lbrakk>\<forall>r \<in> set rs. good r; \<forall>r \<in> set rsa. good r; \<forall>r \<in> set rsb. good r\<rbrakk> \<Longrightarrow>
+rsimp (RALTS (rsa @ rs @ rsb)) = rsimp (RALTS (rsa @ [RALTS rs] @ rsb))"
+  apply(subgoal_tac "rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (map rsimp rsa @ 
+map rsimp rs @ map rsimp rsb)) {})")
+  prefer 2
+  apply simp
+  apply(simp only:)
+    apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp_ALTs (rdistinct (rflts (map rsimp rsa @ 
+[rsimp (RALTS rs)] @ map rsimp rsb)) {})")
+  prefer 2
+   apply simp
+  apply(simp only:)
+  apply(subgoal_tac "map rsimp rsa = rsa")
+  prefer 2
+  apply (simp add: map_idI test)
+  apply(simp only:)
+  apply(subgoal_tac "map rsimp rsb = rsb")
+   prefer 2
+  apply (meson map_idI test)
+  apply(simp only:)
+  apply(subst k00)+
+  apply(subgoal_tac "map rsimp rs = rs")
+   apply(simp only:)
+   prefer 2
+  apply (meson map_idI test)
+  apply(subgoal_tac "rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} = 
+rdistinct (rflts rsa) {} @ rdistinct  (rflts rs @ rflts rsb) (set (rflts rsa))")
+   apply(simp only:)
+  prefer 2
+  using rdistinct_concat_general apply blast
+  apply(subgoal_tac "rdistinct (rflts rsa @ rflts [rsimp (RALTS rs)] @ rflts rsb) {} = 
+rdistinct (rflts rsa) {} @ rdistinct  (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))")
+   apply(simp only:)
+  prefer 2
+  using rdistinct_concat_general apply blast
+  apply(subgoal_tac "rdistinct (rflts rs @ rflts rsb) (set (rflts rsa)) = 
+                     rdistinct  (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))")
+  apply presburger
+  using good_flatten_aux by blast
+
+
+lemma simp_flatten3:
+  shows "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))"
+  apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = 
+                     rsimp (RALTS (map rsimp rsa @ [rsimp (RALTS rs)] @ map rsimp rsb)) ")
+  prefer 2
+   apply (metis append.left_neutral append_Cons list.simps(9) map_append simp_flatten_aux0)
+  apply (simp only:)
+  apply(subgoal_tac "rsimp (RALTS (rsa @ rs @ rsb)) = 
+rsimp (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb))")
+  prefer 2
+   apply (metis map_append simp_flatten_aux0)
+  apply(simp only:)
+  apply(subgoal_tac "rsimp  (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb)) =
+ rsimp (RALTS (map rsimp rsa @ [RALTS (map rsimp rs)] @ map rsimp rsb))")
+  
+   apply (metis (no_types, lifting) head_one_more_simp map_append simp_flatten_aux0)
+  apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsa). good r")
+   apply(subgoal_tac "\<forall>r \<in> set (map rsimp rs). good r")
+    apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsb). good r")
+  
+  using good_flatten_middle apply presburger
+  
+
+  sorry
+
+
+
+  
+
 lemma grewrite_equal_rsimp:
   shows "rs1 \<leadsto>g rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"
   apply(frule grewrite_cases_middle)
lexing