--- a/thys2/ClosedForms.thy Wed Apr 13 22:20:08 2022 +0100
+++ b/thys2/ClosedForms.thy Fri Apr 15 19:35:29 2022 +0100
@@ -2,6 +2,81 @@
"BasicIdentities"
begin
+lemma flts_middle0:
+ shows "rflts (rsa @ RZERO # rsb) = rflts (rsa @ rsb)"
+ apply(induct rsa)
+ 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)
+
+ using simp_flatten apply force
+
+ sorry
+
+inductive
+ hrewrite:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99)
+where
+ "RSEQ RZERO r2 \<leadsto> RZERO"
+| "RSEQ r1 RZERO \<leadsto> RZERO"
+| "RSEQ RONE r \<leadsto> r"
+| "r1 \<leadsto> r2 \<Longrightarrow> RSEQ r1 r3 \<leadsto> RSEQ r2 r3"
+| "r3 \<leadsto> r4 \<Longrightarrow> RSEQ r1 r3 \<leadsto> RSEQ r1 r4"
+| "r \<leadsto> r' \<Longrightarrow> (RALTS (rs1 @ [r] @ rs2)) \<leadsto> (RALTS (rs1 @ [r'] @ rs2))"
+(*context rule for eliminating 0, alts--corresponds to the recursive call flts r::rs = r::(flts rs)*)
+| "RALTS (rsa @ [RZERO] @ rsb) \<leadsto> RALTS (rsa @ rsb)"
+| "RALTS (rsa @ [RALTS rs1] @ rsb) \<leadsto> RALTS (rsa @ rs1 @ rsb)"
+| "RALTS [] \<leadsto> RZERO"
+| "RALTS [r] \<leadsto> r"
+| "a1 = a2 \<Longrightarrow> RALTS (rsa@[a1]@rsb@[a2]@rsc) \<leadsto> RALTS (rsa @ [a1] @ rsb @ rsc)"
+
+inductive
+ hrewrites:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100)
+where
+ rs1[intro, simp]:"r \<leadsto>* r"
+| rs2[intro]: "\<lbrakk>r1 \<leadsto>* r2; r2 \<leadsto> r3\<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"
+
+
+lemma hr_in_rstar : "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"
+ using hrewrites.intros(1) hrewrites.intros(2) by blast
+
+lemma hreal_trans[trans]:
+ assumes a1: "r1 \<leadsto>* r2" and a2: "r2 \<leadsto>* r3"
+ shows "r1 \<leadsto>* r3"
+ using a2 a1
+ apply(induct r2 r3 arbitrary: r1 rule: hrewrites.induct)
+ apply(auto)
+ done
+
+lemma hmany_steps_later: "\<lbrakk>r1 \<leadsto> r2; r2 \<leadsto>* r3 \<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"
+ by (meson hr_in_rstar hreal_trans)
+
+lemma hrewrites_seq_context:
+ shows "r1 \<leadsto>* r2 \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RSEQ r2 r3"
+ apply(induct r1 r2 rule: hrewrites.induct)
+ apply simp
+ using hrewrite.intros(4) by blast
+
+lemma hrewrites_seq_context2:
+ shows "r1 \<leadsto>* r2 \<Longrightarrow> RSEQ r0 r1 \<leadsto>* RSEQ r0 r2"
+ apply(induct r1 r2 rule: hrewrites.induct)
+ apply simp
+ using hrewrite.intros(5) by blast
+
+lemma hrewrites_seq_context0:
+ shows "r1 \<leadsto>* RZERO \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RZERO"
+ apply(subgoal_tac "RSEQ r1 r3 \<leadsto>* RSEQ RZERO r3")
+ using hrewrite.intros(1) apply blast
+ by (simp add: hrewrites_seq_context)
+
+lemma hrewrites_seq_contexts:
+ shows "\<lbrakk>r1 \<leadsto>* r2; r3 \<leadsto>* r4\<rbrakk> \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RSEQ r2 r4"
+ by (meson hreal_trans hrewrites_seq_context hrewrites_seq_context2)
+
+
+
lemma map_concat_cons:
shows "map f rsa @ f a # rs = map f (rsa @ [a]) @ rs"
by simp
@@ -19,11 +94,6 @@
-lemma flts_middle0:
- shows "rflts (rsa @ RZERO # rsb) = rflts (rsa @ rsb)"
- apply(induct rsa)
- apply simp
- by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
lemma flts_middle01:
shows "rflts (rsa @ [RZERO] @ rsb) = rflts (rsa @ rsb)"
@@ -331,17 +401,6 @@
-lemma grewrite_equal_rsimp:
- shows "\<lbrakk>rs1 \<leadsto>g rs2; rsimp_ALTs (rdistinct (rflts (map rsimp rs1)) (rset \<union> \<Union>(alt_set ` rset))) =
- rsimp_ALTs (rdistinct (rflts (map rsimp rs2)) (rset \<union> \<Union>(alt_set ` rset)))\<rbrakk>
- \<Longrightarrow> rsimp_ALTs (rdistinct (rflts (rsimp r # map rsimp rs1)) (rset \<union> \<Union>(alt_set ` rset))) =
- rsimp_ALTs (rdistinct (rflts (rsimp r # map rsimp rs2)) (rset \<union> \<Union>(alt_set ` rset)))"
- apply(induct rs1 rs2 arbitrary:rset rule: grewrite.induct)
- apply simp
- apply (metis append_Cons append_Nil flts_middle0)
- apply(case_tac "rsimp r \<in> rset")
- apply simp
- oops
lemma grewrite_cases_middle:
shows "rs1 \<leadsto>g rs2 \<Longrightarrow>
@@ -1188,13 +1247,6 @@
apply (metis idiot idiot2 rrexp.distinct(5))
by (metis der_simp_nullability rnullable.simps(1) rnullable.simps(4) rsimp.simps(2))
-lemma basic_rsimp_SEQ_property1:
- shows "rsimp_SEQ RONE r = r"
- by (simp add: idiot)
-
-lemma basic_rsimp_SEQ_property3:
- shows "rsimp_SEQ r RZERO = RZERO"
- using rsimp_SEQ.elims by blast
thm rsimp_SEQ.elims
@@ -1270,87 +1322,6 @@
using der_simp_nullability by presburger
-inductive
- hrewrite:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99)
-where
- "RSEQ RZERO r2 \<leadsto> RZERO"
-| "RSEQ r1 RZERO \<leadsto> RZERO"
-| "RSEQ RONE r \<leadsto> r"
-| "r1 \<leadsto> r2 \<Longrightarrow> RSEQ r1 r3 \<leadsto> RSEQ r2 r3"
-| "r3 \<leadsto> r4 \<Longrightarrow> RSEQ r1 r3 \<leadsto> RSEQ r1 r4"
-| "r \<leadsto> r' \<Longrightarrow> (RALTS (rs1 @ [r] @ rs2)) \<leadsto> (RALTS (rs1 @ [r'] @ rs2))"
-(*context rule for eliminating 0, alts--corresponds to the recursive call flts r::rs = r::(flts rs)*)
-| "RALTS (rsa @ [RZERO] @ rsb) \<leadsto> RALTS (rsa @ rsb)"
-| "RALTS (rsa @ [RALTS rs1] @ rsb) \<leadsto> RALTS (rsa @ rs1 @ rsb)"
-| "RALTS [] \<leadsto> RZERO"
-| "RALTS [r] \<leadsto> r"
-| "a1 = a2 \<Longrightarrow> RALTS (rsa@[a1]@rsb@[a2]@rsc) \<leadsto> RALTS (rsa @ [a1] @ rsb @ rsc)"
-
-inductive
- hrewrites:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100)
-where
- rs1[intro, simp]:"r \<leadsto>* r"
-| rs2[intro]: "\<lbrakk>r1 \<leadsto>* r2; r2 \<leadsto> r3\<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"
-
-
-lemma hr_in_rstar : "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"
- using hrewrites.intros(1) hrewrites.intros(2) by blast
-
-lemma hreal_trans[trans]:
- assumes a1: "r1 \<leadsto>* r2" and a2: "r2 \<leadsto>* r3"
- shows "r1 \<leadsto>* r3"
- using a2 a1
- apply(induct r2 r3 arbitrary: r1 rule: hrewrites.induct)
- apply(auto)
- done
-
-lemma hmany_steps_later: "\<lbrakk>r1 \<leadsto> r2; r2 \<leadsto>* r3 \<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"
- by (meson hr_in_rstar hreal_trans)
-
-lemma hrewrites_seq_context:
- shows "r1 \<leadsto>* r2 \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RSEQ r2 r3"
- apply(induct r1 r2 rule: hrewrites.induct)
- apply simp
- using hrewrite.intros(4) by blast
-
-lemma hrewrites_seq_context2:
- shows "r1 \<leadsto>* r2 \<Longrightarrow> RSEQ r0 r1 \<leadsto>* RSEQ r0 r2"
- apply(induct r1 r2 rule: hrewrites.induct)
- apply simp
- using hrewrite.intros(5) by blast
-
-lemma hrewrites_seq_context0:
- shows "r1 \<leadsto>* RZERO \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RZERO"
- apply(subgoal_tac "RSEQ r1 r3 \<leadsto>* RSEQ RZERO r3")
- using hrewrite.intros(1) apply blast
- by (simp add: hrewrites_seq_context)
-
-lemma hrewrites_seq_contexts:
- shows "\<lbrakk>r1 \<leadsto>* r2; r3 \<leadsto>* r4\<rbrakk> \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RSEQ r2 r4"
- by (meson hreal_trans hrewrites_seq_context hrewrites_seq_context2)
-
-lemma hrewrite_simpeq:
- shows "r1 \<leadsto> r2 \<Longrightarrow> rsimp r1 = rsimp r2"
- apply(induct rule: hrewrite.induct)
- apply simp+
- apply (simp add: basic_rsimp_SEQ_property3)
- apply (simp add: basic_rsimp_SEQ_property1)
- using rsimp.simps(1) apply presburger
- apply simp+
- using flts_middle0 apply force
- using simp_flatten3 apply presburger
- apply simp+
- apply (simp add: idem_after_simp1)
- using grewrite.intros(4) grewrite_equal_rsimp by presburger
-
-lemma hrewrites_simpeq:
- shows "r1 \<leadsto>* r2 \<Longrightarrow> rsimp r1 = rsimp r2"
- apply(induct rule: hrewrites.induct)
- apply simp
- apply(subgoal_tac "rsimp r2 = rsimp r3")
- apply auto[1]
- using hrewrite_simpeq by presburger
-
lemma grewrite_ralts:
shows "rs \<leadsto>g rs' \<Longrightarrow> RALTS rs \<leadsto>* RALTS rs'"
@@ -1457,7 +1428,31 @@
(* apply(subgoal_tac "RALTS x \<leadsto>* RALTS (map rsimp x)")*)
-
+lemma hrewrite_simpeq:
+ shows "r1 \<leadsto> r2 \<Longrightarrow> rsimp r1 = rsimp r2"
+ apply(induct rule: hrewrite.induct)
+ apply simp+
+ apply (simp add: basic_rsimp_SEQ_property3)
+ apply (simp add: basic_rsimp_SEQ_property1)
+ using rsimp.simps(1) apply presburger
+ apply simp+
+ using flts_middle0 apply force
+
+
+ using simp_flatten3 apply presburger
+
+ apply simp+
+ apply (simp add: idem_after_simp1)
+ using grewrite.intros(4) grewrite_equal_rsimp by presburger
+
+lemma hrewrites_simpeq:
+ shows "r1 \<leadsto>* r2 \<Longrightarrow> rsimp r1 = rsimp r2"
+ apply(induct rule: hrewrites.induct)
+ apply simp
+ apply(subgoal_tac "rsimp r2 = rsimp r3")
+ apply auto[1]
+ using hrewrite_simpeq by presburger
+
lemma simp_hrewrites:
@@ -2275,4 +2270,5 @@
+
end
\ No newline at end of file