eliminated obsolete fastsimp;
authorwenzelm
Wed May 23 15:57:12 2012 +0200 (2012-05-23)
changeset 47966b8a94ed1646e
parent 47964 b74655182ed6
child 47967 c422128d3889
eliminated obsolete fastsimp;
src/CCL/CCL.thy
src/CCL/Hered.thy
src/CCL/Wfd.thy
src/CCL/ex/Stream.thy
     1.1 --- a/src/CCL/CCL.thy	Wed May 23 15:40:10 2012 +0200
     1.2 +++ b/src/CCL/CCL.thy	Wed May 23 15:57:12 2012 +0200
     1.3 @@ -349,7 +349,7 @@
     1.4  
     1.5  lemma po_lam: "lam x. f(x) [= lam x. f'(x) <-> (ALL x. f(x) [= f'(x))"
     1.6    apply (rule poXH [THEN iff_trans])
     1.7 -  apply fastsimp
     1.8 +  apply fastforce
     1.9    done
    1.10  
    1.11  lemmas ccl_porews = po_bot po_pair po_lam
     2.1 --- a/src/CCL/Hered.thy	Wed May 23 15:40:10 2012 +0200
     2.2 +++ b/src/CCL/Hered.thy	Wed May 23 15:57:12 2012 +0200
     2.3 @@ -118,13 +118,13 @@
     2.4    by (simp add: subsetXH UnitXH HTT_rews)
     2.5  
     2.6  lemma BoolF: "Bool <= HTT"
     2.7 -  by (fastsimp simp: subsetXH BoolXH iff: HTT_rews)
     2.8 +  by (fastforce simp: subsetXH BoolXH iff: HTT_rews)
     2.9  
    2.10  lemma PlusF: "[| A <= HTT;  B <= HTT |] ==> A + B  <= HTT"
    2.11 -  by (fastsimp simp: subsetXH PlusXH iff: HTT_rews)
    2.12 +  by (fastforce simp: subsetXH PlusXH iff: HTT_rews)
    2.13  
    2.14  lemma SigmaF: "[| A <= HTT;  !!x. x:A ==> B(x) <= HTT |] ==> SUM x:A. B(x) <= HTT"
    2.15 -  by (fastsimp simp: subsetXH SgXH HTT_rews)
    2.16 +  by (fastforce simp: subsetXH SgXH HTT_rews)
    2.17  
    2.18  
    2.19  (*** Formation Rules for Recursive types - using coinduction these only need ***)
    2.20 @@ -135,7 +135,7 @@
    2.21    apply (simp add: subsetXH)
    2.22    apply clarify
    2.23    apply (erule Nat_ind)
    2.24 -   apply (fastsimp iff: HTT_rews)+
    2.25 +   apply (fastforce iff: HTT_rews)+
    2.26    done
    2.27  
    2.28  lemma NatF: "Nat <= HTT"
     3.1 --- a/src/CCL/Wfd.thy	Wed May 23 15:40:10 2012 +0200
     3.2 +++ b/src/CCL/Wfd.thy	Wed May 23 15:57:12 2012 +0200
     3.3 @@ -209,18 +209,18 @@
     3.4    apply (unfold Wfd_def)
     3.5    apply clarify
     3.6    apply (tactic {* wfd_strengthen_tac @{context} "%x. x:Nat" 1 *})
     3.7 -   apply (fastsimp iff: NatPRXH)
     3.8 +   apply (fastforce iff: NatPRXH)
     3.9    apply (erule Nat_ind)
    3.10 -   apply (fastsimp iff: NatPRXH)+
    3.11 +   apply (fastforce iff: NatPRXH)+
    3.12    done
    3.13  
    3.14  lemma ListPR_wf: "Wfd(ListPR(A))"
    3.15    apply (unfold Wfd_def)
    3.16    apply clarify
    3.17    apply (tactic {* wfd_strengthen_tac @{context} "%x. x:List (A)" 1 *})
    3.18 -   apply (fastsimp iff: ListPRXH)
    3.19 +   apply (fastforce iff: ListPRXH)
    3.20    apply (erule List_ind)
    3.21 -   apply (fastsimp iff: ListPRXH)+
    3.22 +   apply (fastforce iff: ListPRXH)+
    3.23    done
    3.24  
    3.25  
     4.1 --- a/src/CCL/ex/Stream.thy	Wed May 23 15:40:10 2012 +0200
     4.2 +++ b/src/CCL/ex/Stream.thy	Wed May 23 15:57:12 2012 +0200
     4.3 @@ -33,7 +33,7 @@
     4.4    apply safe
     4.5    apply (drule ListsXH [THEN iffD1])
     4.6    apply (tactic "EQgen_tac @{context} [] 1")
     4.7 -   apply fastsimp
     4.8 +   apply fastforce
     4.9    done
    4.10  
    4.11  (*** Mapping the identity function leaves a list unchanged ***)