Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/IOA/meta_theory/CompoTraces.thy
changeset 35215 a03462cbf86f
parent 35174 e15040ae75d7
child 35642 f478d5a9d238 
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Thu Feb 18 12:36:09 2010 -0800
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Thu Feb 18 13:29:59 2010 -0800
@@ -207,18 +207,18 @@
 (* a:A, a:B *)
 apply simp
 apply (rule Forall_Conc_impl [THEN mp])
-apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
+apply (simp add: intA_is_not_actB int_is_act)
 apply (rule Forall_Conc_impl [THEN mp])
-apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
+apply (simp add: intA_is_not_actB int_is_act)
 (* a:A,a~:B *)
 apply simp
 apply (rule Forall_Conc_impl [THEN mp])
-apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
+apply (simp add: intA_is_not_actB int_is_act)
 apply (case_tac "a:act B")
 (* a~:A, a:B *)
 apply simp
 apply (rule Forall_Conc_impl [THEN mp])
-apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
+apply (simp add: intA_is_not_actB int_is_act)
 (* a~:A,a~:B *)
 apply auto
 done
@@ -230,7 +230,7 @@
   [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
 apply auto
 apply (rule Forall_Conc_impl [THEN mp])
-apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
+apply (simp add: intA_is_not_actB int_is_act)
 done
 
 lemma ForallAnBmksch [rule_format (no_asm)]: "!!A B. compatible A B ==>  
@@ -240,7 +240,7 @@
   [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
 apply auto
 apply (rule Forall_Conc_impl [THEN mp])
-apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
+apply (simp add: intA_is_not_actB int_is_act)
 done
 
 (* safe-tac makes too many case distinctions with this lemma in the next proof *)
@@ -345,14 +345,12 @@
 apply (rule_tac x = "Takewhile (%a. a:int B) $y @@ a>>y1" in exI)
 apply (rule_tac x = "y2" in exI)
 (* elminate all obligations up to two depending on Conc_assoc *)
-apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act int_is_not_ext FilterConc)
+apply (simp add: intA_is_not_actB int_is_act int_is_not_ext FilterConc)
 apply (simp (no_asm) add: Conc_assoc FilterConc)
 done
 
 lemmas reduceA_mksch = conjI [THEN [6] conjI [THEN [5] reduceA_mksch1]]
 
-declare FilterConc [simp del]
-
 lemma reduceB_mksch1 [rule_format]:
 " [| Finite a_s; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>   
  ! x. Forall (%x. x:act A) x & Forall (%x. x:act A & x~:act B) a_s & 
@@ -393,7 +391,7 @@
 apply (rule_tac x = "Takewhile (%a. a:int A) $x @@ a>>x1" in exI)
 apply (rule_tac x = "x2" in exI)
 (* elminate all obligations up to two depending on Conc_assoc *)
-apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act int_is_not_ext FilterConc)
+apply (simp add: intA_is_not_actB int_is_act int_is_not_ext FilterConc)
 apply (simp (no_asm) add: Conc_assoc FilterConc)
 done
 
@@ -573,7 +571,7 @@
 apply (rule take_reduction)
 
 (* f A (tw iA) = tw ~eA *)
-apply (simp add: FilterPTakewhileQid int_is_act not_ext_is_int_or_not_act)
+apply (simp add: int_is_act not_ext_is_int_or_not_act)
 apply (rule refl)
 apply (simp add: int_is_act not_ext_is_int_or_not_act)
 apply (rotate_tac -11)
@@ -582,7 +580,7 @@
 
 (* assumption Forall tr *)
 (* assumption schB *)
-apply (simp add: Forall_Conc ext_and_act)
+apply (simp add: ext_and_act)
 (* assumption schA *)
 apply (drule_tac x = "schA" and g = "Filter (%a. a:act A) $rs" in subst_lemma2)
 apply assumption
@@ -595,7 +593,7 @@
 (* assumption Forall schA *)
 apply (drule_tac s = "schA" and P = "Forall (%x. x:act A) " in subst)
 apply assumption
-apply (simp add: ForallPTakewhileQ int_is_act)
+apply (simp add: int_is_act)
 
 (* case x:actions(asig_of A) & x: actions(asig_of B) *)
 
@@ -623,7 +621,7 @@
 apply assumption
 
 (* f A (tw iA) = tw ~eA *)
-apply (simp add: FilterPTakewhileQid int_is_act not_ext_is_int_or_not_act)
+apply (simp add: int_is_act not_ext_is_int_or_not_act)
 
 (* rewrite assumption forall and schB *)
 apply (rotate_tac 13)
@@ -792,7 +790,7 @@
 apply (rule take_reduction)
 
 (* f B (tw iB) = tw ~eB *)
-apply (simp add: FilterPTakewhileQid int_is_act not_ext_is_int_or_not_act)
+apply (simp add: int_is_act not_ext_is_int_or_not_act)
 apply (rule refl)
 apply (simp add: int_is_act not_ext_is_int_or_not_act)
 apply (rotate_tac -11)
@@ -800,7 +798,7 @@
 (* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
 
 (* assumption schA *)
-apply (simp add: Forall_Conc ext_and_act)
+apply (simp add: ext_and_act)
 (* assumption schB *)
 apply (drule_tac x = "schB" and g = "Filter (%a. a:act B) $rs" in subst_lemma2)
 apply assumption
@@ -813,7 +811,7 @@
 (* assumption Forall schB *)
 apply (drule_tac s = "schB" and P = "Forall (%x. x:act B) " in subst)
 apply assumption
-apply (simp add: ForallPTakewhileQ int_is_act)
+apply (simp add: int_is_act)
 
 (* case x:actions(asig_of A) & x: actions(asig_of B) *)
 
@@ -840,7 +838,7 @@
 apply assumption
 
 (* f B (tw iB) = tw ~eB *)
-apply (simp add: FilterPTakewhileQid int_is_act not_ext_is_int_or_not_act)
+apply (simp add: int_is_act not_ext_is_int_or_not_act)
 
 (* rewrite assumption forall and schB *)
 apply (rotate_tac 13)
isabelle