src/HOL/IMP/Fold.thy

 
 
 lemma defs_restrict:
   "defs c t |` (- lnames c) = t |` (- lnames c)"
 proof (induction c arbitrary: t)
-  case (Semi c1 c2)
+  case (Seq c1 c2)
   hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)" 
     by simp
   hence "defs c1 t |` (- lnames c1) |` (-lnames c2) = 
          t |` (- lnames c1) |` (-lnames c2)" by simp
   moreover
-  from Semi
+  from Seq
   have "defs c2 (defs c1 t) |` (- lnames c2) = 
         defs c1 t |` (- lnames c2)"
     by simp
   hence "defs c2 (defs c1 t) |` (- lnames c2) |` (- lnames c1) =
          defs c1 t |` (- lnames c2) |` (- lnames c1)"

 next
   case Assign
   thus ?case
     by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split)
 next
-  case (Semi c1 s1 s2 c2 s3)
-  have "approx (defs c1 t) s2" by (rule Semi.IH(1)[OF Semi.prems])
-  hence "approx (defs c2 (defs c1 t)) s3" by (rule Semi.IH(2))
+  case (Seq c1 s1 s2 c2 s3)
+  have "approx (defs c1 t) s2" by (rule Seq.IH(1)[OF Seq.prems])
+  hence "approx (defs c2 (defs c1 t)) s3" by (rule Seq.IH(2))
   thus ?case by simp
 next
   case (IfTrue b s c1 s')
   hence "approx (defs c1 t) s'" by simp
   thus ?case by (simp add: approx_merge)

   "(c,s) \<Rightarrow> s' \<Longrightarrow> approx (t |` (-lnames c)) s \<Longrightarrow> approx (t |` (-lnames c)) s'"
 proof (induction arbitrary: t rule: big_step_induct)
   case Assign
   thus ?case by (clarsimp simp: approx_def)
 next
-  case (Semi c1 s1 s2 c2 s3)
+  case (Seq c1 s1 s2 c2 s3)
   hence "approx (t |` (-lnames c2) |` (-lnames c1)) s1" 
     by (simp add: Int_commute)
   hence "approx (t |` (-lnames c2) |` (-lnames c1)) s2"
-    by (rule Semi)
+    by (rule Seq)
   hence "approx (t |` (-lnames c1) |` (-lnames c2)) s2"
     by (simp add: Int_commute)
   hence "approx (t |` (-lnames c1) |` (-lnames c2)) s3"
-    by (rule Semi)
+    by (rule Seq)
   thus ?case by simp
 next
   case (IfTrue b s c1 s' c2)
   hence "approx (t |` (-lnames c2) |` (-lnames c1)) s" 
     by (simp add: Int_commute)

   case SKIP show ?case by simp
 next
   case Assign
   show ?case by (simp add: equiv_up_to_def)
 next
-  case Semi 
-  thus ?case by (auto intro!: equiv_up_to_semi)
+  case Seq 
+  thus ?case by (auto intro!: equiv_up_to_seq)
 next
   case If
   thus ?case by (auto intro!: equiv_up_to_if_weak)
 next
   case (While b c)

 
 
 lemma bdefs_restrict:
   "bdefs c t |` (- lnames c) = t |` (- lnames c)"
 proof (induction c arbitrary: t)
-  case (Semi c1 c2)
+  case (Seq c1 c2)
   hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)" 
     by simp
   hence "bdefs c1 t |` (- lnames c1) |` (-lnames c2) = 
          t |` (- lnames c1) |` (-lnames c2)" by simp
   moreover
-  from Semi
+  from Seq
   have "bdefs c2 (bdefs c1 t) |` (- lnames c2) = 
         bdefs c1 t |` (- lnames c2)"
     by simp
   hence "bdefs c2 (bdefs c1 t) |` (- lnames c2) |` (- lnames c1) =
          bdefs c1 t |` (- lnames c2) |` (- lnames c1)"

 next
   case Assign
   thus ?case
     by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split)
 next
-  case (Semi c1 s1 s2 c2 s3)
-  have "approx (bdefs c1 t) s2" by (rule Semi.IH(1)[OF Semi.prems])
-  hence "approx (bdefs c2 (bdefs c1 t)) s3" by (rule Semi.IH(2))
+  case (Seq c1 s1 s2 c2 s3)
+  have "approx (bdefs c1 t) s2" by (rule Seq.IH(1)[OF Seq.prems])
+  hence "approx (bdefs c2 (bdefs c1 t)) s3" by (rule Seq.IH(2))
   thus ?case by simp
 next
   case (IfTrue b s c1 s')
   hence "approx (bdefs c1 t) s'" by simp
   thus ?case using `bval b s` `approx t s`

   case SKIP show ?case by simp
 next
   case Assign
   thus ?case by (simp add: equiv_up_to_def)
 next
-  case Semi
-  thus ?case by (auto intro!: equiv_up_to_semi)           
+  case Seq
+  thus ?case by (auto intro!: equiv_up_to_seq)           
 next
   case (If b c1 c2)
   hence "approx t \<Turnstile> IF b THEN c1 ELSE c2 \<sim> 
                    IF Fold.bsimp_const b t THEN bfold c1 t ELSE bfold c2 t"
     by (auto intro: equiv_up_to_if_weak simp: bequiv_up_to_def)