conversion ML -> thy
authornipkow
Mon Oct 28 14:29:51 2002 +0100 (2002-10-28)
changeset 1368291674c8a008b
parent 13681 06cce9be31a4
child 13683 47fdf4e8e89c
conversion ML -> thy
src/HOL/Hoare/Examples.thy
src/HOL/Hoare/Hoare.thy
src/HOL/Hoare/Pointers.thy
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/Hoare/Examples.thy	Sun Oct 27 23:34:02 2002 +0100
     1.2 +++ b/src/HOL/Hoare/Examples.thy	Mon Oct 28 14:29:51 2002 +0100
     1.3 @@ -6,4 +6,207 @@
     1.4  Various examples.
     1.5  *)
     1.6  
     1.7 -Examples = Hoare + Arith2
     1.8 +theory Examples = Hoare + Arith2:
     1.9 +
    1.10 +(*** ARITHMETIC ***)
    1.11 +
    1.12 +(** multiplication by successive addition **)
    1.13 +
    1.14 +lemma multiply_by_add: "|- VARS m s a b.
    1.15 +  {a=A & b=B}
    1.16 +  m := 0; s := 0;
    1.17 +  WHILE m~=a
    1.18 +  INV {s=m*b & a=A & b=B}
    1.19 +  DO s := s+b; m := m+(1::nat) OD
    1.20 +  {s = A*B}"
    1.21 +by vcg_simp
    1.22 +
    1.23 +
    1.24 +(** Euclid's algorithm for GCD **)
    1.25 +
    1.26 +lemma Euclid_GCD: "|- VARS a b.
    1.27 + {0<A & 0<B}
    1.28 + a := A; b := B;
    1.29 + WHILE  a~=b
    1.30 + INV {0<a & 0<b & gcd A B = gcd a b}
    1.31 + DO IF a<b THEN b := b-a ELSE a := a-b FI OD
    1.32 + {a = gcd A B}"
    1.33 +apply vcg
    1.34 +(*Now prove the verification conditions*)
    1.35 +  apply auto
    1.36 +  apply(simp add: gcd_diff_r less_imp_le)
    1.37 + apply(simp add: not_less_iff_le gcd_diff_l)
    1.38 +apply(erule gcd_nnn)
    1.39 +done
    1.40 +
    1.41 +(** Dijkstra's extension of Euclid's algorithm for simultaneous GCD and SCM **)
    1.42 +(* From E.W. Disjkstra. Selected Writings on Computing, p 98 (EWD474),
    1.43 +   where it is given without the invariant. Instead of defining scm
    1.44 +   explicitly we have used the theorem scm x y = x*y/gcd x y and avoided
    1.45 +   division by mupltiplying with gcd x y.
    1.46 +*)
    1.47 +
    1.48 +lemmas distribs =
    1.49 +  diff_mult_distrib diff_mult_distrib2 add_mult_distrib add_mult_distrib2
    1.50 +
    1.51 +lemma gcd_scm: "|- VARS a b x y.
    1.52 + {0<A & 0<B & a=A & b=B & x=B & y=A}
    1.53 + WHILE  a ~= b
    1.54 + INV {0<a & 0<b & gcd A B = gcd a b & 2*A*B = a*x + b*y}
    1.55 + DO IF a<b THEN (b := b-a; x := x+y) ELSE (a := a-b; y := y+x) FI OD
    1.56 + {a = gcd A B & 2*A*B = a*(x+y)}"
    1.57 +apply vcg
    1.58 +  apply simp
    1.59 + apply(simp add: distribs gcd_diff_r not_less_iff_le gcd_diff_l)
    1.60 + apply arith
    1.61 +apply(simp add: distribs gcd_nnn)
    1.62 +done
    1.63 +
    1.64 +(** Power by iterated squaring and multiplication **)
    1.65 +
    1.66 +lemma power_by_mult: "|- VARS a b c.
    1.67 + {a=A & b=B}
    1.68 + c := (1::nat);
    1.69 + WHILE b ~= 0
    1.70 + INV {A^B = c * a^b}
    1.71 + DO  WHILE b mod 2 = 0
    1.72 +     INV {A^B = c * a^b}
    1.73 +     DO  a := a*a; b := b div 2 OD;
    1.74 +     c := c*a; b := b - 1
    1.75 + OD
    1.76 + {c = A^B}"
    1.77 +apply vcg_simp
    1.78 +apply(case_tac "b")
    1.79 + apply(simp add: mod_less)
    1.80 +apply simp
    1.81 +done
    1.82 +
    1.83 +(** Factorial **)
    1.84 +
    1.85 +lemma factorial: "|- VARS a b.
    1.86 + {a=A}
    1.87 + b := 1;
    1.88 + WHILE a ~= 0
    1.89 + INV {fac A = b * fac a}
    1.90 + DO b := b*a; a := a - 1 OD
    1.91 + {b = fac A}"
    1.92 +apply vcg_simp
    1.93 +apply(clarsimp split: nat_diff_split)
    1.94 +done
    1.95 +
    1.96 +
    1.97 +(** Square root **)
    1.98 +
    1.99 +(* the easy way: *)
   1.100 +
   1.101 +lemma sqrt: "|- VARS r x.
   1.102 + {True}
   1.103 + x := X; r := (0::nat);
   1.104 + WHILE (r+1)*(r+1) <= x
   1.105 + INV {r*r <= x & x=X}
   1.106 + DO r := r+1 OD
   1.107 + {r*r <= X & X < (r+1)*(r+1)}"
   1.108 +apply vcg_simp
   1.109 +apply auto
   1.110 +done
   1.111 +
   1.112 +(* without multiplication *)
   1.113 +
   1.114 +lemma sqrt_without_multiplication: "|- VARS u w r x.
   1.115 + {True}
   1.116 + x := X; u := 1; w := 1; r := (0::nat);
   1.117 + WHILE w <= x
   1.118 + INV {u = r+r+1 & w = (r+1)*(r+1) & r*r <= x & x=X}
   1.119 + DO r := r + 1; w := w + u + 2; u := u + 2 OD
   1.120 + {r*r <= X & X < (r+1)*(r+1)}"
   1.121 +apply vcg_simp
   1.122 +apply auto
   1.123 +done
   1.124 +
   1.125 +
   1.126 +(*** LISTS ***)
   1.127 +
   1.128 +lemma imperative_reverse: "|- VARS y x.
   1.129 + {x=X}
   1.130 + y:=[];
   1.131 + WHILE x ~= []
   1.132 + INV {rev(x)@y = rev(X)}
   1.133 + DO y := (hd x # y); x := tl x OD
   1.134 + {y=rev(X)}"
   1.135 +apply vcg_simp
   1.136 + apply(simp add: neq_Nil_conv)
   1.137 + apply auto
   1.138 +done
   1.139 +
   1.140 +lemma imperative_append: "|- VARS x y.
   1.141 + {x=X & y=Y}
   1.142 + x := rev(x);
   1.143 + WHILE x~=[]
   1.144 + INV {rev(x)@y = X@Y}
   1.145 + DO y := (hd x # y);
   1.146 +    x := tl x
   1.147 + OD
   1.148 + {y = X@Y}"
   1.149 +apply vcg_simp
   1.150 +apply(simp add: neq_Nil_conv)
   1.151 +apply auto
   1.152 +done
   1.153 +
   1.154 +
   1.155 +(*** ARRAYS ***)
   1.156 +
   1.157 +(* Search for a key *)
   1.158 +lemma zero_search: "|- VARS A i.
   1.159 + {True}
   1.160 + i := 0;
   1.161 + WHILE i < length A & A!i ~= key
   1.162 + INV {!j. j<i --> A!j ~= key}
   1.163 + DO i := i+1 OD
   1.164 + {(i < length A --> A!i = key) &
   1.165 +  (i = length A --> (!j. j < length A --> A!j ~= key))}"
   1.166 +apply vcg_simp
   1.167 +apply(blast elim!: less_SucE)
   1.168 +done
   1.169 +
   1.170 +(* 
   1.171 +The `partition' procedure for quicksort.
   1.172 +`A' is the array to be sorted (modelled as a list).
   1.173 +Elements of A must be of class order to infer at the end
   1.174 +that the elements between u and l are equal to pivot.
   1.175 +
   1.176 +Ambiguity warnings of parser are due to := being used
   1.177 +both for assignment and list update.
   1.178 +*)
   1.179 +lemma lem: "m - Suc 0 < n ==> m < Suc n"
   1.180 +by arith
   1.181 +
   1.182 +
   1.183 +lemma Partition:
   1.184 +"[| leq == %A i. !k. k<i --> A!k <= pivot;
   1.185 +    geq == %A i. !k. i<k & k<length A --> pivot <= A!k |] ==>
   1.186 + |- VARS A u l.
   1.187 + {0 < length(A::('a::order)list)}
   1.188 + l := 0; u := length A - Suc 0;
   1.189 + WHILE l <= u
   1.190 +  INV {leq A l & geq A u & u<length A & l<=length A}
   1.191 +  DO WHILE l < length A & A!l <= pivot
   1.192 +     INV {leq A l & geq A u & u<length A & l<=length A}
   1.193 +     DO l := l+1 OD;
   1.194 +     WHILE 0 < u & pivot <= A!u
   1.195 +     INV {leq A l & geq A u  & u<length A & l<=length A}
   1.196 +     DO u := u - 1 OD;
   1.197 +     IF l <= u THEN A := A[l := A!u, u := A!l] ELSE SKIP FI
   1.198 +  OD
   1.199 + {leq A u & (!k. u<k & k<l --> A!k = pivot) & geq A l}"
   1.200 +(* expand and delete abbreviations first *)
   1.201 +apply (simp);
   1.202 +apply (erule thin_rl)+
   1.203 +apply vcg_simp
   1.204 +    apply (force simp: neq_Nil_conv)
   1.205 +   apply (blast elim!: less_SucE intro: Suc_leI)
   1.206 +  apply (blast elim!: less_SucE intro: less_imp_diff_less dest: lem)
   1.207 + apply (force simp: nth_list_update)
   1.208 +apply (auto intro: order_antisym)
   1.209 +done
   1.210 +
   1.211 +end
   1.212 \ No newline at end of file
     2.1 --- a/src/HOL/Hoare/Hoare.thy	Sun Oct 27 23:34:02 2002 +0100
     2.2 +++ b/src/HOL/Hoare/Hoare.thy	Mon Oct 28 14:29:51 2002 +0100
     2.3 @@ -9,34 +9,34 @@
     2.4  later.
     2.5  *)
     2.6  
     2.7 -Hoare  = Main +
     2.8 +theory Hoare  = Main
     2.9 +files ("Hoare.ML"):
    2.10  
    2.11  types
    2.12 -    'a bexp = 'a set
    2.13 -    'a assn = 'a set
    2.14 -    'a fexp = 'a =>'a
    2.15 +    'a bexp = "'a set"
    2.16 +    'a assn = "'a set"
    2.17  
    2.18  datatype
    2.19 - 'a com = Basic ('a fexp)         
    2.20 -   | Seq ('a com) ('a com)               ("(_;/ _)"      [61,60] 60)
    2.21 -   | Cond ('a bexp) ('a com) ('a com)    ("(1IF _/ THEN _ / ELSE _/ FI)"  [0,0,0] 61)
    2.22 -   | While ('a bexp) ('a assn) ('a com)  ("(1WHILE _/ INV {_} //DO _ /OD)"  [0,0,0] 61)
    2.23 + 'a com = Basic "'a \<Rightarrow> 'a"         
    2.24 +   | Seq "'a com" "'a com"               ("(_;/ _)"      [61,60] 60)
    2.25 +   | Cond "'a bexp" "'a com" "'a com"    ("(1IF _/ THEN _ / ELSE _/ FI)"  [0,0,0] 61)
    2.26 +   | While "'a bexp" "'a assn" "'a com"  ("(1WHILE _/ INV {_} //DO _ /OD)"  [0,0,0] 61)
    2.27    
    2.28  syntax
    2.29 -  "@assign"  :: id => 'b => 'a com        ("(2_ :=/ _)" [70,65] 61)
    2.30 -  "@annskip" :: 'a com                    ("SKIP")
    2.31 +  "@assign"  :: "id => 'b => 'a com"        ("(2_ :=/ _)" [70,65] 61)
    2.32 +  "@annskip" :: "'a com"                    ("SKIP")
    2.33  
    2.34  translations
    2.35              "SKIP" == "Basic id"
    2.36  
    2.37 -types 'a sem = 'a => 'a => bool
    2.38 +types 'a sem = "'a => 'a => bool"
    2.39  
    2.40 -consts iter :: nat => 'a bexp => 'a sem => 'a sem
    2.41 +consts iter :: "nat => 'a bexp => 'a sem => 'a sem"
    2.42  primrec
    2.43  "iter 0 b S = (%s s'. s ~: b & (s=s'))"
    2.44  "iter (Suc n) b S = (%s s'. s : b & (? s''. S s s'' & iter n b S s'' s'))"
    2.45  
    2.46 -consts Sem :: 'a com => 'a sem
    2.47 +consts Sem :: "'a com => 'a sem"
    2.48  primrec
    2.49  "Sem(Basic f) s s' = (s' = f s)"
    2.50  "Sem(c1;c2) s s' = (? s''. Sem c1 s s'' & Sem c2 s'' s')"
    2.51 @@ -44,7 +44,7 @@
    2.52                                        (s ~: b --> Sem c2 s s'))"
    2.53  "Sem(While b x c) s s' = (? n. iter n b (Sem c) s s')"
    2.54  
    2.55 -constdefs Valid :: ['a bexp, 'a com, 'a bexp] => bool
    2.56 +constdefs Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
    2.57    "Valid p c q == !s s'. Sem c s s' --> s : p --> s' : q"
    2.58  
    2.59  
    2.60 @@ -56,18 +56,15 @@
    2.61    "_vars" 	     :: "[id, vars] => vars"	       ("_ _")
    2.62  
    2.63  syntax
    2.64 - "@hoare_vars" :: [vars, 'a assn,'a com,'a assn] => bool
    2.65 + "@hoare_vars" :: "[vars, 'a assn,'a com,'a assn] => bool"
    2.66                   ("|- VARS _.// {_} // _ // {_}" [0,0,55,0] 50)
    2.67  syntax ("" output)
    2.68 - "@hoare"      :: ['a assn,'a com,'a assn] => bool
    2.69 + "@hoare"      :: "['a assn,'a com,'a assn] => bool"
    2.70                   ("|- {_} // _ // {_}" [0,55,0] 50)
    2.71  
    2.72 -end
    2.73 -
    2.74 -ML
    2.75 -
    2.76  (** parse translations **)
    2.77  
    2.78 +ML{*
    2.79  fun mk_abstuple []     body = absfree ("x", dummyT, body)
    2.80    | mk_abstuple [v]    body = absfree ((fst o dest_Free) v, dummyT, body)
    2.81    | mk_abstuple (v::w) body = Syntax.const "split" $
    2.82 @@ -80,19 +77,20 @@
    2.83                             mk_fbody v e xs;
    2.84  
    2.85  fun mk_fexp v e xs = mk_abstuple xs (mk_fbody v e xs);
    2.86 -
    2.87 +*}
    2.88  
    2.89  (* bexp_tr & assn_tr *)
    2.90  (*all meta-variables for bexp except for TRUE are translated as if they
    2.91    were boolean expressions*)
    2.92 -  
    2.93 +ML{*
    2.94  fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE"
    2.95    | bexp_tr b xs = Syntax.const "Collect" $ mk_abstuple xs b;
    2.96    
    2.97  fun assn_tr r xs = Syntax.const "Collect" $ mk_abstuple xs r;
    2.98 +*}
    2.99  
   2.100  (* com_tr *)
   2.101 -  
   2.102 +ML{*
   2.103  fun assign_tr [Free (V,_),E] xs = Syntax.const "Basic" $
   2.104                                        mk_fexp (Free(V,dummyT)) E xs
   2.105    | assign_tr ts _ = raise TERM ("assign_tr", ts);
   2.106 @@ -107,9 +105,10 @@
   2.107    | com_tr (Const ("While",_) $ b $ I $ c) xs = Syntax.const "While" $
   2.108                                           bexp_tr b xs $ assn_tr I xs $ com_tr c xs
   2.109    | com_tr trm _ = trm;
   2.110 +*}
   2.111  
   2.112  (* triple_tr *)
   2.113 -
   2.114 +ML{*
   2.115  fun vars_tr (x as Free _) = [x]
   2.116    | vars_tr (Const ("_vars", _) $ (x as Free _) $ vars) = x :: vars_tr vars
   2.117    | vars_tr t = raise TERM ("vars_tr", [t]);
   2.118 @@ -120,16 +119,15 @@
   2.119             assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
   2.120        end
   2.121    | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
   2.122 -  
   2.123 +*}
   2.124  
   2.125 -
   2.126 -val parse_translation = [("@hoare_vars", hoare_vars_tr)];
   2.127 +parse_translation {* [("@hoare_vars", hoare_vars_tr)] *}
   2.128  
   2.129  
   2.130  (*****************************************************************************)
   2.131  
   2.132  (*** print translations ***)
   2.133 -
   2.134 +ML{*
   2.135  fun dest_abstuple (Const ("split",_) $ (Abs(v,_, body))) =
   2.136                              subst_bound (Syntax.free v, dest_abstuple body)
   2.137    | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body)
   2.138 @@ -156,9 +154,10 @@
   2.139  fun is_f (Const ("split",_) $ (Abs(x,_,t))) = true
   2.140    | is_f (Abs(x,_,t)) = true
   2.141    | is_f t = false;
   2.142 -  
   2.143 +*}
   2.144 +
   2.145  (* assn_tr' & bexp_tr'*)
   2.146 -  
   2.147 +ML{*  
   2.148  fun assn_tr' (Const ("Collect",_) $ T) = dest_abstuple T
   2.149    | assn_tr' (Const ("op Int",_) $ (Const ("Collect",_) $ T1) $ 
   2.150                                     (Const ("Collect",_) $ T2)) =  
   2.151 @@ -167,9 +166,10 @@
   2.152  
   2.153  fun bexp_tr' (Const ("Collect",_) $ T) = dest_abstuple T 
   2.154    | bexp_tr' t = t;
   2.155 +*}
   2.156  
   2.157  (*com_tr' *)
   2.158 -
   2.159 +ML{*
   2.160  fun mk_assign f =
   2.161    let val (vs, ts) = mk_vts f;
   2.162        val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs)
   2.163 @@ -189,5 +189,21 @@
   2.164  
   2.165  fun spec_tr' [p, c, q] =
   2.166    Syntax.const "@hoare" $ assn_tr' p $ com_tr' c $ assn_tr' q
   2.167 - 
   2.168 -val print_translation = [("Valid", spec_tr')];
   2.169 +*}
   2.170 +
   2.171 +print_translation {* [("Valid", spec_tr')] *}
   2.172 +
   2.173 +use "Hoare.ML"
   2.174 +
   2.175 +method_setup vcg = {*
   2.176 +  Method.no_args
   2.177 +    (Method.SIMPLE_METHOD' HEADGOAL (hoare_tac (K all_tac))) *}
   2.178 +  "verification condition generator"
   2.179 +
   2.180 +method_setup vcg_simp = {*
   2.181 +  Method.ctxt_args (fn ctxt =>
   2.182 +    Method.METHOD (fn facts => 
   2.183 +      hoare_tac (asm_full_simp_tac (Simplifier.get_local_simpset ctxt))1)) *}
   2.184 +  "verification condition generator plus simplification"
   2.185 +
   2.186 +end
     3.1 --- a/src/HOL/Hoare/Pointers.thy	Sun Oct 27 23:34:02 2002 +0100
     3.2 +++ b/src/HOL/Hoare/Pointers.thy	Mon Oct 28 14:29:51 2002 +0100
     3.3 @@ -94,13 +94,27 @@
     3.4  
     3.5  section"Hoare logic"
     3.6  
     3.7 -(* This should already be done in Hoare.thy, which should be converted to
     3.8 -Isar *)
     3.9 +consts fac :: "nat \<Rightarrow> nat"
    3.10 +primrec
    3.11 +"fac 0 = 1"
    3.12 +"fac (Suc n) = Suc n * fac n"
    3.13 +
    3.14 +lemma [simp]: "1 \<le> i \<Longrightarrow> fac (i - Suc 0) * i = fac i"
    3.15 +by(induct i, simp_all)
    3.16  
    3.17 -method_setup vcg_simp_tac = {*
    3.18 -  Method.no_args
    3.19 -    (Method.SIMPLE_METHOD' HEADGOAL (hoare_tac Asm_full_simp_tac)) *}
    3.20 -  "verification condition generator plus simplification"
    3.21 +lemma "|- VARS i f.
    3.22 + {True}
    3.23 + i := (1::nat); f := 1;
    3.24 + WHILE i <= n INV {f = fac(i - 1) & 1 <= i & i <= n+1}
    3.25 + DO f := f*i; i := i+1 OD
    3.26 + {f = fac n}"
    3.27 +apply vcg_simp
    3.28 +apply(subgoal_tac "i = Suc n")
    3.29 +apply simp
    3.30 +apply arith
    3.31 +done
    3.32 +
    3.33 +
    3.34  
    3.35  subsection"List reversal"
    3.36  
    3.37 @@ -111,7 +125,7 @@
    3.38                   rev As' @ Bs' = rev As @ Bs}
    3.39    DO r := p; p := tl(the p); tl := tl(the r := q); q := r OD
    3.40    {list tl q (rev As @ Bs)}"
    3.41 -apply vcg_simp_tac
    3.42 +apply vcg_simp
    3.43  
    3.44  apply(rule_tac x = As in exI)
    3.45  apply simp
    3.46 @@ -144,7 +158,7 @@
    3.47    INV {p ~= None & (\<exists>As'. list tl p As' \<and> X \<in> set As')}
    3.48    DO p := tl(the p) OD
    3.49    {p = Some X}"
    3.50 -apply vcg_simp_tac
    3.51 +apply vcg_simp
    3.52    apply(case_tac p)
    3.53     apply clarsimp
    3.54    apply fastsimp
    3.55 @@ -162,7 +176,7 @@
    3.56    INV {p ~= None & (\<exists>As'. path tl p As' (Some X))}
    3.57    DO p := tl(the p) OD
    3.58    {p = Some X}"
    3.59 -apply vcg_simp_tac
    3.60 +apply vcg_simp
    3.61    apply(case_tac p)
    3.62     apply clarsimp
    3.63    apply(rule conjI)
    3.64 @@ -195,7 +209,7 @@
    3.65    INV {p ~= None & Some X \<in> ({(Some x,tl x) |x. True}^* `` {p})}
    3.66    DO p := tl(the p) OD
    3.67    {p = Some X}"
    3.68 -apply vcg_simp_tac
    3.69 +apply vcg_simp
    3.70    apply(case_tac p)
    3.71     apply(simp add:lem1 eq_sym_conv)
    3.72    apply simp
    3.73 @@ -214,7 +228,7 @@
    3.74    INV {p ~= None & X \<in> ({(x,y). tl x = Some y}^* `` {the p})}
    3.75    DO p := tl(the p) OD
    3.76    {p = Some X}"
    3.77 -apply vcg_simp_tac
    3.78 +apply vcg_simp
    3.79   apply clarsimp
    3.80   apply(erule converse_rtranclE)
    3.81    apply simp
     4.1 --- a/src/HOL/IsaMakefile	Sun Oct 27 23:34:02 2002 +0100
     4.2 +++ b/src/HOL/IsaMakefile	Mon Oct 28 14:29:51 2002 +0100
     4.3 @@ -293,7 +293,7 @@
     4.4  HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz
     4.5  
     4.6  $(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.ML Hoare/Arith2.thy \
     4.7 -  Hoare/Examples.ML Hoare/Examples.thy Hoare/Hoare.ML Hoare/Hoare.thy \
     4.8 +  Hoare/Examples.thy Hoare/Hoare.ML Hoare/Hoare.thy \
     4.9    Hoare/Pointers.thy Hoare/ROOT.ML
    4.10  	@$(ISATOOL) usedir $(OUT)/HOL Hoare
    4.11