src/HOL/Hoare/Pointer_Examples.thy
changeset 44890 22f665a2e91c
parent 41959 b460124855b8
child 62042 6c6ccf573479
     1.1 --- a/src/HOL/Hoare/Pointer_Examples.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/Hoare/Pointer_Examples.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -23,20 +23,20 @@
     1.4    DO r := p; p := p^.tl; r^.tl := q; q := r OD
     1.5    {List tl q (rev Ps @ Qs)}"
     1.6  apply vcg_simp
     1.7 -  apply fastsimp
     1.8 - apply(fastsimp intro:notin_List_update[THEN iffD2])
     1.9 +  apply fastforce
    1.10 + apply(fastforce intro:notin_List_update[THEN iffD2])
    1.11  (* explicit:
    1.12   apply clarify
    1.13   apply(rename_tac ps b qs)
    1.14   apply clarsimp
    1.15   apply(rename_tac ps')
    1.16 - apply(fastsimp intro:notin_List_update[THEN iffD2])
    1.17 + apply(fastforce intro:notin_List_update[THEN iffD2])
    1.18   apply(rule_tac x = ps' in exI)
    1.19   apply simp
    1.20   apply(rule_tac x = "b#qs" in exI)
    1.21   apply simp
    1.22  *)
    1.23 -apply fastsimp
    1.24 +apply fastforce
    1.25  done
    1.26  
    1.27  text{* And now with ghost variables @{term ps} and @{term qs}. Even
    1.28 @@ -52,8 +52,8 @@
    1.29       qs := (hd ps) # qs; ps := tl ps OD
    1.30    {List next q (rev Ps @ Qs)}"
    1.31  apply vcg_simp
    1.32 - apply fastsimp
    1.33 -apply fastsimp
    1.34 + apply fastforce
    1.35 +apply fastforce
    1.36  done
    1.37  
    1.38  text "A longer readable version:"
    1.39 @@ -69,7 +69,7 @@
    1.40    fix tl p q r
    1.41    assume "List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}"
    1.42    thus "\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
    1.43 -                rev ps @ qs = rev Ps @ Qs" by fastsimp
    1.44 +                rev ps @ qs = rev Ps @ Qs" by fastforce
    1.45  next
    1.46    fix tl p q r
    1.47    assume "(\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
    1.48 @@ -77,12 +77,12 @@
    1.49           (is "(\<exists>ps qs. ?I ps qs) \<and> _")
    1.50    then obtain ps qs a where I: "?I ps qs \<and> p = Ref a"
    1.51      by fast
    1.52 -  then obtain ps' where "ps = a # ps'" by fastsimp
    1.53 +  then obtain ps' where "ps = a # ps'" by fastforce
    1.54    hence "List (tl(p \<rightarrow> q)) (p^.tl) ps' \<and>
    1.55           List (tl(p \<rightarrow> q)) p       (a#qs) \<and>
    1.56           set ps' \<inter> set (a#qs) = {} \<and>
    1.57           rev ps' @ (a#qs) = rev Ps @ Qs"
    1.58 -    using I by fastsimp
    1.59 +    using I by fastforce
    1.60    thus "\<exists>ps' qs'. List (tl(p \<rightarrow> q)) (p^.tl) ps' \<and>
    1.61                    List (tl(p \<rightarrow> q)) p       qs' \<and>
    1.62                    set ps' \<inter> set qs' = {} \<and>
    1.63 @@ -91,7 +91,7 @@
    1.64    fix tl p q r
    1.65    assume "(\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
    1.66                     rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> Null"
    1.67 -  thus "List tl q (rev Ps @ Qs)" by fastsimp
    1.68 +  thus "List tl q (rev Ps @ Qs)" by fastforce
    1.69  qed
    1.70  
    1.71  
    1.72 @@ -144,7 +144,7 @@
    1.73    {p = X}"
    1.74  apply vcg_simp
    1.75    apply blast
    1.76 - apply fastsimp
    1.77 + apply fastforce
    1.78  apply clarsimp
    1.79  done
    1.80  
    1.81 @@ -196,7 +196,7 @@
    1.82    {List tl p (splice Ps Qs)}"
    1.83  apply vcg_simp
    1.84    apply(rule_tac x = "[]" in exI)
    1.85 -  apply fastsimp
    1.86 +  apply fastforce
    1.87   apply clarsimp
    1.88   apply(rename_tac y bs qqs)
    1.89   apply(case_tac bs) apply simp
    1.90 @@ -208,7 +208,7 @@
    1.91   apply simp
    1.92   apply(rule_tac x = "qqs" in exI)
    1.93   apply simp
    1.94 -apply (fastsimp simp:List_app)
    1.95 +apply (fastforce simp:List_app)
    1.96  done
    1.97  
    1.98  
    1.99 @@ -259,13 +259,13 @@
   1.100  apply vcg_simp
   1.101  apply (simp_all add: cand_def cor_def)
   1.102  
   1.103 -apply (fastsimp)
   1.104 +apply (fastforce)
   1.105  
   1.106  apply clarsimp
   1.107  apply(rule conjI)
   1.108  apply clarsimp
   1.109  apply(rule conjI)
   1.110 -apply (fastsimp intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
   1.111 +apply (fastforce intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
   1.112  apply clarsimp
   1.113  apply(rule conjI)
   1.114  apply (clarsimp)
   1.115 @@ -282,7 +282,7 @@
   1.116  apply(clarsimp simp:eq_sym_conv)
   1.117  apply(rule_tac x = "bsa" in exI)
   1.118  apply(simp)
   1.119 -apply (fastsimp intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
   1.120 +apply (fastforce intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
   1.121  
   1.122  apply(clarsimp simp add:List_app)
   1.123  done
   1.124 @@ -311,7 +311,7 @@
   1.125  apply vcg_simp
   1.126  apply (simp_all add: cand_def cor_def)
   1.127  
   1.128 -apply (fastsimp)
   1.129 +apply (fastforce)
   1.130  
   1.131  apply clarsimp
   1.132  apply(rule conjI)
   1.133 @@ -393,8 +393,8 @@
   1.134  apply vcg_simp
   1.135  
   1.136  apply (simp_all add: cand_def cor_def)
   1.137 -  apply (fastsimp)
   1.138 - apply (fastsimp simp: eq_sym_conv)
   1.139 +  apply (fastforce)
   1.140 + apply (fastforce simp: eq_sym_conv)
   1.141  apply(clarsimp)
   1.142  done
   1.143  
   1.144 @@ -470,7 +470,7 @@
   1.145    apply clarsimp
   1.146    apply clarsimp
   1.147   apply (case_tac "(q = Null)")
   1.148 -  apply (fastsimp intro: Path_is_List)
   1.149 +  apply (fastforce intro: Path_is_List)
   1.150   apply clarsimp
   1.151   apply (rule_tac x= "bs" in exI)
   1.152   apply (rule_tac x= "y # qs" in exI)
   1.153 @@ -506,7 +506,7 @@
   1.154    {islist next p \<and> map elem (rev(list next p)) = Xs}"
   1.155  apply vcg_simp
   1.156   apply (clarsimp simp: subset_insert_iff neq_Nil_conv fun_upd_apply new_notin)
   1.157 -apply fastsimp
   1.158 +apply fastforce
   1.159  done
   1.160  
   1.161