New directory.
Hoare logic according to Mike Gordon.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/Arith2.ML Fri Nov 17 09:04:10 1995 +0100
@@ -0,0 +1,400 @@
+(* Title: HOL/Hoare/Arith2.ML
+ ID: $Id$
+ Author: Norbert Galm
+ Copyright 1995 TUM
+
+More arithmetic lemmas.
+*)
+
+open Arith2;
+
+
+(*** HOL lemmas ***)
+
+
+val [prem1,prem2]=goal HOL.thy "[|~P ==> ~Q; Q|] ==> P";
+by (cut_facts_tac [prem1 COMP impI,prem2] 1);
+by (fast_tac HOL_cs 1);
+val not_imp_swap=result();
+
+
+(*** analogue of diff_induct, for simultaneous induction over 3 vars ***)
+
+val prems = goal Nat.thy
+ "[| !!x. P x 0 0; \
+\ !!y. P 0 (Suc y) 0; \
+\ !!z. P 0 0 (Suc z); \
+\ !!x y. [| P x y 0 |] ==> P (Suc x) (Suc y) 0; \
+\ !!x z. [| P x 0 z |] ==> P (Suc x) 0 (Suc z); \
+\ !!y z. [| P 0 y z |] ==> P 0 (Suc y) (Suc z); \
+\ !!x y z. [| P x y z |] ==> P (Suc x) (Suc y) (Suc z) \
+\ |] ==> P m n k";
+by (res_inst_tac [("x","m")] spec 1);
+br diff_induct 1;
+br allI 1;
+br allI 2;
+by (res_inst_tac [("m","xa"),("n","x")] diff_induct 1);
+by (res_inst_tac [("m","x"),("n","Suc y")] diff_induct 4);
+br allI 7;
+by (nat_ind_tac "xa" 7);
+by (ALLGOALS (resolve_tac prems));
+ba 1;
+ba 1;
+by (fast_tac HOL_cs 1);
+by (fast_tac HOL_cs 1);
+qed "diff_induct3";
+
+(*** interaction of + and - ***)
+
+val prems=goal Arith.thy "~m<n+k ==> (m - n) - k = m - ((n + k)::nat)";
+by (cut_facts_tac prems 1);
+br mp 1;
+ba 2;
+by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
+by (ALLGOALS Asm_simp_tac);
+qed "diff_not_assoc";
+
+val prems=goal Arith.thy "[|~m<n; ~n<k|] ==> (m - n) + k = m - ((n - k)::nat)";
+by (cut_facts_tac prems 1);
+bd conjI 1;
+ba 1;
+by (res_inst_tac [("P","~m<n & ~n<k")] mp 1);
+ba 2;
+by (res_inst_tac [("m","m"),("n","n"),("k","k")] diff_induct3 1);
+by (ALLGOALS Asm_simp_tac);
+br impI 1;
+by (dres_inst_tac [("P","~x<y")] conjE 1);
+ba 2;
+br (Suc_diff_n RS sym) 1;
+br le_less_trans 1;
+be (not_less_eq RS subst) 2;
+br (hd ([diff_less_Suc RS lessD] RL [Suc_le_mono RS subst])) 1;
+qed "diff_add_not_assoc";
+
+val prems=goal Arith.thy "~n<k ==> (m + n) - k = m + ((n - k)::nat)";
+by (cut_facts_tac prems 1);
+br mp 1;
+ba 2;
+by (res_inst_tac [("m","n"),("n","k")] diff_induct 1);
+by (ALLGOALS Asm_simp_tac);
+qed "add_diff_assoc";
+
+(*** more ***)
+
+val prems = goal Arith.thy "m~=(n::nat) = (m<n | n<m)";
+br iffI 1;
+by (cut_inst_tac [("m","m"),("n","n")] less_linear 1);
+by (Asm_full_simp_tac 1);
+be disjE 1;
+be (less_not_refl2 RS not_sym) 1;
+be less_not_refl2 1;
+qed "not_eq_eq_less_or_gr";
+
+val [prem] = goal Arith.thy "m<n ==> n-m~=0";
+by (rtac (prem RS rev_mp) 1);
+by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
+by (ALLGOALS Asm_simp_tac);
+qed "less_imp_diff_not_0";
+
+(*******************************************************************)
+
+val prems = goal Arith.thy "(i::nat)<j ==> k+i<k+j";
+by (cut_facts_tac prems 1);
+by (nat_ind_tac "k" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "add_less_mono_l";
+
+val prems = goal Arith.thy "~(i::nat)<j ==> ~k+i<k+j";
+by (cut_facts_tac prems 1);
+by (nat_ind_tac "k" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "add_not_less_mono_l";
+
+val prems = goal Arith.thy "[|0<k; m<(n::nat)|] ==> m*k<n*k";
+by (cut_facts_tac prems 1);
+by (res_inst_tac [("n","k")] natE 1);
+by (ALLGOALS Asm_full_simp_tac);
+by (nat_ind_tac "x" 1);
+be add_less_mono 2;
+by (ALLGOALS Asm_full_simp_tac);
+qed "mult_less_mono_r";
+
+val prems = goal Arith.thy "~m<(n::nat) ==> ~m*k<n*k";
+by (cut_facts_tac prems 1);
+by (nat_ind_tac "k" 1);
+by (ALLGOALS Simp_tac);
+by (fold_goals_tac [le_def]);
+be add_le_mono 1;
+ba 1;
+qed "mult_not_less_mono_r";
+
+val prems = goal Arith.thy "m=(n::nat) ==> m*k=n*k";
+by (cut_facts_tac prems 1);
+by (nat_ind_tac "k" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "mult_eq_mono_r";
+
+val prems = goal Arith.thy "[|0<k; m~=(n::nat)|] ==> m*k~=n*k";
+by (cut_facts_tac prems 1);
+by (res_inst_tac [("P","m<n"),("Q","n<m")] disjE 1);
+br (less_not_refl2 RS not_sym) 2;
+be mult_less_mono_r 2;
+br less_not_refl2 3;
+be mult_less_mono_r 3;
+by (ALLGOALS (asm_full_simp_tac ((simpset_of "Arith") addsimps [not_eq_eq_less_or_gr])));
+qed "mult_not_eq_mono_r";
+
+(******************************************************************)
+
+val prems = goal Arith.thy "(m - n)*k = (m*k) - ((n*k)::nat)";
+by (res_inst_tac [("P","m*k<n*k")] case_split_thm 1);
+by (forward_tac [mult_not_less_mono_r COMP not_imp_swap] 1);
+bd (less_not_sym RS (not_less_eq RS iffD1) RS less_imp_diff_is_0) 1;
+bd (less_not_sym RS (not_less_eq RS iffD1) RS less_imp_diff_is_0) 1;
+br mp 2;
+ba 3;
+by (res_inst_tac [("m","m"),("n","n")] diff_induct 2);
+by (ALLGOALS Asm_simp_tac);
+br impI 1;
+bd (refl RS iffD1) 1;
+by (dres_inst_tac [("k","k")] add_not_less_mono_l 1);
+bd (refl RS iffD1) 1;
+bd (refl RS iffD1) 1;
+bd diff_not_assoc 1;
+by (asm_full_simp_tac ((simpset_of "Arith") addsimps [diff_add_inverse]) 1);
+qed "diff_mult_distrib_r";
+
+
+(*** mod ***)
+
+(* Alternativ-Beweis zu mod_nn_is_0: Spezialfall zu mod_prod_nn_is_0 *)
+(*
+val prems = goal thy "0<n ==> n mod n = 0";
+by (cut_inst_tac [("m","Suc(0)")] (mod_prod_nn_is_0 COMP impI) 1);
+by (cut_facts_tac prems 1);
+by (Asm_full_simp_tac 1);
+by (fast_tac HOL_cs 1);
+*)
+
+val prems=goal thy "0<n ==> n mod n = 0";
+by (cut_facts_tac prems 1);
+br (mod_def RS wf_less_trans) 1;
+by (asm_full_simp_tac ((simpset_of "Arith") addsimps [diff_self_eq_0,cut_def,less_eq]) 1);
+be mod_less 1;
+qed "mod_nn_is_0";
+
+val prems=goal thy "0<n ==> m mod n = (m+n) mod n";
+by (cut_facts_tac prems 1);
+by (res_inst_tac [("s","n+m"),("t","m+n")] subst 1);
+br add_commute 1;
+by (res_inst_tac [("s","n+m-n"),("P","%x.x mod n = (n + m) mod n")] subst 1);
+br diff_add_inverse 1;
+br sym 1;
+be mod_geq 1;
+by (res_inst_tac [("s","n<=n+m"),("t","~n+m<n")] subst 1);
+by (simp_tac ((simpset_of "Arith") addsimps [le_def]) 1);
+br le_add1 1;
+qed "mod_eq_add";
+
+val prems=goal thy "0<n ==> m*n mod n = 0";
+by (cut_facts_tac prems 1);
+by (nat_ind_tac "m" 1);
+by (Simp_tac 1);
+be mod_less 1;
+by (dres_inst_tac [("n","n"),("m","m1*n")] mod_eq_add 1);
+by (asm_full_simp_tac ((simpset_of "Arith") addsimps [add_commute]) 1);
+qed "mod_prod_nn_is_0";
+
+val prems=goal thy "[|0<x; m mod x = 0; n mod x = 0|] ==> (m+n) mod x = 0";
+by (cut_facts_tac prems 1);
+by (res_inst_tac [("s","m div x * x + m mod x"),("t","m")] subst 1);
+be mod_div_equality 1;
+by (res_inst_tac [("s","n div x * x + n mod x"),("t","n")] subst 1);
+be mod_div_equality 1;
+by (Asm_simp_tac 1);
+by (res_inst_tac [("s","(m div x + n div x) * x"),("t","m div x * x + n div x * x")] subst 1);
+br add_mult_distrib 1;
+be mod_prod_nn_is_0 1;
+qed "mod0_sum";
+
+val prems=goal thy "[|0<x; m mod x = 0; n mod x = 0; n<=m|] ==> (m-n) mod x = 0";
+by (cut_facts_tac prems 1);
+by (res_inst_tac [("s","m div x * x + m mod x"),("t","m")] subst 1);
+be mod_div_equality 1;
+by (res_inst_tac [("s","n div x * x + n mod x"),("t","n")] subst 1);
+be mod_div_equality 1;
+by (Asm_simp_tac 1);
+by (res_inst_tac [("s","(m div x - n div x) * x"),("t","m div x * x - n div x * x")] subst 1);
+br diff_mult_distrib_r 1;
+be mod_prod_nn_is_0 1;
+qed "mod0_diff";
+
+
+(*** div ***)
+
+val prems = goal thy "0<n ==> m*n div n = m";
+by (cut_facts_tac prems 1);
+br (mult_not_eq_mono_r RS not_imp_swap) 1;
+ba 1;
+ba 1;
+by (res_inst_tac [("P","%x.m*n div n * n = x")] (mod_div_equality RS subst) 1);
+ba 1;
+by (dres_inst_tac [("m","m")] mod_prod_nn_is_0 1);
+by (Asm_simp_tac 1);
+qed "div_prod_nn_is_m";
+
+
+(*** divides ***)
+
+val prems=goalw thy [divides_def] "0<n ==> n divides n";
+by (cut_facts_tac prems 1);
+by (forward_tac [mod_nn_is_0] 1);
+by (Asm_simp_tac 1);
+qed "divides_nn";
+
+val prems=goalw thy [divides_def] "x divides n ==> x<=n";
+by (cut_facts_tac prems 1);
+br ((mod_less COMP rev_contrapos) RS (le_def RS meta_eq_to_obj_eq RS iffD2)) 1;
+by (Asm_simp_tac 1);
+br (less_not_refl2 RS not_sym) 1;
+by (Asm_simp_tac 1);
+qed "divides_le";
+
+val prems=goalw thy [divides_def] "[|x divides m; x divides n|] ==> x divides (m+n)";
+by (cut_facts_tac prems 1);
+by (REPEAT ((dtac conjE 1) THEN (atac 2)));
+br conjI 1;
+by (dres_inst_tac [("m","0"),("n","m")] less_imp_add_less 1);
+ba 1;
+be conjI 1;
+br mod0_sum 1;
+by (ALLGOALS atac);
+qed "divides_sum";
+
+val prems=goalw thy [divides_def] "[|x divides m; x divides n; n<m|] ==> x divides (m-n)";
+by (cut_facts_tac prems 1);
+by (REPEAT ((dtac conjE 1) THEN (atac 2)));
+br conjI 1;
+be less_imp_diff_positive 1;
+be conjI 1;
+br mod0_diff 1;
+by (ALLGOALS (asm_simp_tac ((simpset_of "Arith") addsimps [le_def])));
+be less_not_sym 1;
+qed "divides_diff";
+
+
+(*** cd ***)
+
+
+val prems=goalw thy [cd_def] "0<n ==> cd n n n";
+by (cut_facts_tac prems 1);
+bd divides_nn 1;
+by (Asm_simp_tac 1);
+qed "cd_nnn";
+
+val prems=goalw thy [cd_def] "cd x m n ==> x<=m & x<=n";
+by (cut_facts_tac prems 1);
+bd conjE 1;
+ba 2;
+bd divides_le 1;
+bd divides_le 1;
+by (Asm_simp_tac 1);
+qed "cd_le";
+
+val prems=goalw thy [cd_def] "cd x m n = cd x n m";
+by (fast_tac HOL_cs 1);
+qed "cd_swap";
+
+val prems=goalw thy [cd_def] "n<m ==> cd x m n = cd x (m-n) n";
+by (cut_facts_tac prems 1);
+br iffI 1;
+bd conjE 1;
+ba 2;
+br conjI 1;
+br divides_diff 1;
+bd conjE 5;
+ba 6;
+br conjI 5;
+bd less_not_sym 5;
+bd add_diff_inverse 5;
+by (dres_inst_tac [("m","n"),("n","m-n")] divides_sum 5);
+by (ALLGOALS Asm_full_simp_tac);
+qed "cd_diff_l";
+
+val prems=goalw thy [cd_def] "m<n ==> cd x m n = cd x m (n-m)";
+by (cut_facts_tac prems 1);
+br iffI 1;
+bd conjE 1;
+ba 2;
+br conjI 1;
+br divides_diff 2;
+bd conjE 5;
+ba 6;
+br conjI 5;
+bd less_not_sym 6;
+bd add_diff_inverse 6;
+by (dres_inst_tac [("n","n-m")] divides_sum 6);
+by (ALLGOALS Asm_full_simp_tac);
+qed "cd_diff_r";
+
+
+(*** gcd ***)
+
+val prems = goalw thy [gcd_def] "0<n ==> n = gcd n n";
+by (cut_facts_tac prems 1);
+bd cd_nnn 1;
+br (select_equality RS sym) 1;
+be conjI 1;
+br allI 1;
+br impI 1;
+bd cd_le 1;
+bd conjE 2;
+ba 3;
+br le_anti_sym 2;
+by (dres_inst_tac [("x","x")] cd_le 2);
+by (dres_inst_tac [("x","n")] spec 3);
+by (ALLGOALS Asm_full_simp_tac);
+qed "gcd_nnn";
+
+val prems = goalw thy [gcd_def] "gcd m n = gcd n m";
+by (simp_tac ((simpset_of "Arith") addsimps [cd_swap]) 1);
+qed "gcd_swap";
+
+val prems=goalw thy [gcd_def] "n<m ==> gcd m n = gcd (m-n) n";
+by (cut_facts_tac prems 1);
+by (subgoal_tac "n<m ==> !x.cd x m n = cd x (m-n) n" 1);
+by (Asm_simp_tac 1);
+br allI 1;
+be cd_diff_l 1;
+qed "gcd_diff_l";
+
+val prems=goalw thy [gcd_def] "m<n ==> gcd m n = gcd m (n-m)";
+by (cut_facts_tac prems 1);
+by (subgoal_tac "m<n ==> !x.cd x m n = cd x m (n-m)" 1);
+by (Asm_simp_tac 1);
+br allI 1;
+be cd_diff_r 1;
+qed "gcd_diff_r";
+
+
+(*** pow ***)
+
+val [pow_0,pow_Suc] = nat_recs pow_def;
+store_thm("pow_0",pow_0);
+store_thm("pow_Suc",pow_Suc);
+
+goalw thy [pow_def] "m pow (n+k) = m pow n * m pow k";
+by (nat_ind_tac "k" 1);
+by (ALLGOALS (asm_simp_tac ((simpset_of "Arith") addsimps [mult_left_commute])));
+qed "pow_add_reduce";
+
+goalw thy [pow_def] "m pow n pow k = m pow (n*k)";
+by (nat_ind_tac "k" 1);
+by (ALLGOALS Asm_simp_tac);
+by (fold_goals_tac [pow_def]);
+br (pow_add_reduce RS sym) 1;
+qed "pow_pow_reduce";
+
+(*** fac ***)
+
+Addsimps(nat_recs fac_def);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/Arith2.thy Fri Nov 17 09:04:10 1995 +0100
@@ -0,0 +1,27 @@
+(* Title: HOL/Hoare/Arith2.thy
+ ID: $Id$
+ Author: Norbert Galm
+ Copyright 1995 TUM
+
+More arithmetic.
+*)
+
+Arith2 = Arith +
+
+consts
+ divides :: "[nat, nat] => bool" (infixl 70)
+ cd :: "[nat, nat, nat] => bool"
+ gcd :: "[nat, nat] => nat"
+
+ pow :: "[nat, nat] => nat" (infixl 75)
+ fac :: "nat => nat"
+
+defs
+ divides_def "x divides n == 0<n & 0<x & (n mod x) = 0"
+ cd_def "cd x m n == x divides m & x divides n"
+ gcd_def "gcd m n == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
+
+ pow_def "m pow n == nat_rec n (Suc 0) (%u v.m*v)"
+ fac_def "fac m == nat_rec m (Suc 0) (%u v.(Suc u)*v)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/Examples.ML Fri Nov 17 09:04:10 1995 +0100
@@ -0,0 +1,120 @@
+(* Title: HOL/Hoare/Examples.thy
+ ID: $Id$
+ Author: Norbert Galm
+ Copyright 1995 TUM
+
+Various arithmetic examples.
+*)
+
+open Examples;
+
+(*** multiplication by successive addition ***)
+
+goal thy
+ "{m=0 & s=0} \
+\ WHILE m ~= a DO {s = m*b} s := s+b; m := Suc(m) END\
+\ {s = a*b}";
+by(hoare_tac 1);
+by(ALLGOALS (asm_full_simp_tac (!simpset addsimps add_ac)));
+qed "multiply_by_add";
+
+
+(*** Euclid's algorithm for GCD ***)
+
+goal thy
+" {0<A & 0<B & a=A & b=B} \
+\ WHILE a ~= b \
+\ DO {0<a & 0<b & gcd A B = gcd a b} \
+\ IF a<b \
+\ THEN \
+\ b:=b-a \
+\ ELSE \
+\ a:=a-b \
+\ END \
+\ END \
+\ {a = gcd A B}";
+
+by (hoare_tac 1);
+
+by (safe_tac HOL_cs);
+
+be less_imp_diff_positive 1;
+be gcd_diff_r 1;
+
+by (cut_facts_tac [less_linear] 1);
+by (cut_facts_tac [less_linear] 2);
+br less_imp_diff_positive 1;
+br gcd_diff_l 2;
+
+bd gcd_nnn 3;
+
+by (ALLGOALS (fast_tac HOL_cs));
+
+qed "Euclid_GCD";
+
+
+(*** Power by interated squaring and multiplication ***)
+
+goal thy
+" {a=A & b=B} \
+\ c:=1; \
+\ WHILE b~=0 \
+\ DO {A pow B = c * a pow b} \
+\ WHILE b mod 2=0 \
+\ DO {A pow B = c * a pow b} \
+\ a:=a*a; \
+\ b:=b div 2 \
+\ END; \
+\ c:=c*a; \
+\ b:=b-1 \
+\ END \
+\ {c = A pow B}";
+
+by (hoare_tac 1);
+
+by (simp_tac ((simpset_of "Arith") addsimps [pow_0]) 3);
+
+by (safe_tac HOL_cs);
+
+by (subgoal_tac "a*a=a pow 2" 1);
+by (Asm_simp_tac 1);
+br (pow_pow_reduce RS ssubst) 1;
+
+by (subgoal_tac "(b div 2)*2=b" 1);
+by (subgoal_tac "0<2" 2);
+by (dres_inst_tac [("m","b")] mod_div_equality 2);
+
+by (ALLGOALS (asm_full_simp_tac ((simpset_of "Arith") addsimps [pow_0,pow_Suc,mult_assoc])));
+
+by (subgoal_tac "b~=0" 1);
+by (res_inst_tac [("n","b")] natE 1);
+by (res_inst_tac [("Q","b mod 2 ~= 0")] not_imp_swap 3);
+ba 4;
+
+by (ALLGOALS (asm_full_simp_tac ((simpset_of "Arith") addsimps [pow_0,pow_Suc,mult_assoc])));
+br mod_less 1;
+by (Simp_tac 1);
+
+qed "power_by_mult";
+
+(*** factorial ***)
+
+goal thy
+" {a=A} \
+\ b:=1; \
+\ WHILE a~=0 \
+\ DO {fac A = b*fac a} \
+\ b:=b*a; \
+\ a:=a-1 \
+\ END \
+\ {b = fac A}";
+
+by (hoare_tac 1);
+
+by (safe_tac HOL_cs);
+
+by (res_inst_tac [("n","a")] natE 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [mult_assoc])));
+by (fast_tac HOL_cs 1);
+
+qed"factorial";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/Examples.thy Fri Nov 17 09:04:10 1995 +0100
@@ -0,0 +1,20 @@
+(* Title: HOL/Hoare/Examples.thy
+ ID: $Id$
+ Author: Norbert Galm
+ Copyright 1995 TUM
+
+Various arithmetic examples.
+*)
+
+Examples = Hoare + Arith2 +
+
+syntax
+ "@1" :: "nat" ("1")
+ "@2" :: "nat" ("2")
+
+translations
+ "1" == "Suc(0)"
+ "2" == "Suc(Suc(0))"
+end
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/Hoare.ML Fri Nov 17 09:04:10 1995 +0100
@@ -0,0 +1,254 @@
+(* Title: HOL/Hoare/Hoare.ML
+ ID: $Id$
+ Author: Norbert Galm & Tobias Nipkow
+ Copyright 1995 TUM
+
+The verification condition generation tactics.
+*)
+
+open Hoare;
+
+(*** Hoare rules ***)
+
+val SkipRule = prove_goalw thy [SpecDef,SkipDef]
+ "(!!s.p(s) ==> q(s)) ==> Spec p Skip q"
+ (fn prems => [fast_tac (HOL_cs addIs prems) 1]);
+
+val AssignRule = prove_goalw thy [SpecDef,AssignDef]
+ "(!!s. p s ==> q(%x.if x=v then e s else s x)) ==> Spec p (Assign v e) q"
+ (fn prems => [fast_tac (HOL_cs addIs prems) 1]);
+
+val SeqRule = prove_goalw thy [SpecDef,SeqDef]
+ "[| Spec p c (%s.q s); Spec (%s.q s) c' r |] ==> Spec p (Seq c c') r"
+ (fn prems => [cut_facts_tac prems 1, fast_tac HOL_cs 1]);
+
+val IfRule = prove_goalw thy [SpecDef,CondDef]
+ "[| !!s. p s ==> (b s --> q s) & (~b s --> q' s); \
+\ Spec (%s.q s) c r; Spec (%s.q' s) c' r |] \
+\ ==> Spec p (Cond b c c') r"
+ (fn [prem1,prem2,prem3] =>
+ [REPEAT (rtac allI 1),
+ REPEAT (rtac impI 1),
+ dresolve_tac [prem1] 1,
+ cut_facts_tac [prem2,prem3] 1,
+ fast_tac (HOL_cs addIs [prem1]) 1]);
+
+val strenthen_pre = prove_goalw thy [SpecDef]
+ "[| !!s. p s ==> p' s; Spec p' c q |] ==> Spec p c q"
+ (fn [prem1,prem2] =>[cut_facts_tac [prem2] 1,
+ fast_tac (HOL_cs addIs [prem1]) 1]);
+
+val [iter_0,iter_Suc] = nat_recs IterDef;
+
+val lemma = prove_goalw thy [SpecDef,WhileDef]
+ "[| Spec (%s.inv s & b s) c inv; !!s. [| inv s; ~b s |] ==> q s |] \
+\ ==> Spec inv (While b inv c) q"
+ (fn [prem1,prem2] =>
+ [REPEAT(rtac allI 1), rtac impI 1, etac exE 1, rtac mp 1, atac 2,
+ etac thin_rl 1, res_inst_tac[("x","s")]spec 1,
+ res_inst_tac[("x","s'")]spec 1, nat_ind_tac "n" 1,
+ simp_tac (!simpset addsimps [iter_0]) 1,
+ fast_tac (HOL_cs addIs [prem2]) 1,
+ simp_tac (!simpset addsimps [iter_Suc,SeqDef]) 1,
+ cut_facts_tac [prem1] 1, fast_tac (HOL_cs addIs [prem2]) 1]);
+
+val WhileRule = lemma RSN (2,strenthen_pre);
+
+
+(*** meta_spec used in StateElimTac ***)
+
+val meta_spec = prove_goal HOL.thy
+ "(!!s x. PROP P s x) ==> (!!s. PROP P s (x s))"
+ (fn prems => [resolve_tac prems 1]);
+
+
+(**************************************************************************************************)
+(*** Funktion zum Generieren eines Theorems durch Umbennenen von Namen von Lambda-Abstraktionen ***)
+(*** in einem bestehenden Theorem. Bsp.: "!a.?P(a) ==> ?P(?x)" aus "!x.?P(x) ==> ?P(?x)" ***)
+(**************************************************************************************************)
+
+(* rename_abs:term (von:string,nach:string,trm:term) benennt in trm alle Lambda-Abstraktionen
+ mit Namen von in nach um *)
+
+fun rename_abs (von,nach,Abs (s,t,trm)) =if von=s
+ then Abs (nach,t,rename_abs (von,nach,trm))
+ else Abs (s,t,rename_abs (von,nach,trm))
+ | rename_abs (von,nach,trm1 $ trm2) =rename_abs (von,nach,trm1) $ rename_abs (von,nach,trm2)
+ | rename_abs (_,_,trm) =trm;
+
+(* ren_abs_thm:thm (von:string,nach:string,theorem:thm) benennt in theorem alle Lambda-Abstraktionen
+ mit Namen von in nach um. Vorgehen:
+ - Term t zu thoerem bestimmen
+ - Term t' zu t durch Umbenennen der Namen generieren
+ - Certified Term ct' zu t' erstellen
+ - Thoerem ct'==ct' anlegen
+ - Nach der Regel "[|P==Q; P|] ==> Q" wird aus "ct'==ct'" und theorem das Theorem zu ct'
+ abgeleitet (ist moeglich, da t' mit t unifiziert werden kann, da nur Umnbenennungen) *)
+
+fun ren_abs_thm (von,nach,theorem) =
+ equal_elim
+ (
+ reflexive (
+ cterm_of
+ (#sign (rep_thm theorem))
+ (rename_abs (von,nach,#prop (rep_thm theorem)))
+ )
+ )
+ theorem;
+
+
+(**************************************************************************************************)
+(*** Taktik zum Anwenden eines Theorems theorem auf ein Subgoal i durch ***)
+(*** - Umbenennen von Lambda-Abstraktionen im Theorem ***)
+(*** - Instanziieren von freien Variablen im Theorem ***)
+(*** - Composing des Subgoals mit dem Theorem ***)
+(**************************************************************************************************)
+
+(* - rens:(string*string) list, d.h. es koennen verschiedene Lambda-Abstraktionen umbenannt werden
+ - insts:(cterm*cterm) list, d.h. es koennen verschiedene Variablen instanziiert werden *)
+
+fun comp_inst_ren_tac rens insts theorem i =
+ let
+ fun compose_inst_ren_tac [] insts theorem i =
+ compose_tac (false,cterm_instantiate insts theorem,nprems_of theorem) i
+ | compose_inst_ren_tac ((von,nach)::rl) insts theorem i =
+ compose_inst_ren_tac rl insts (ren_abs_thm (von,nach,theorem)) i
+ in
+ compose_inst_ren_tac rens insts theorem i
+ end;
+
+
+(**************************************************************************************************)
+(*** Taktik zum Eliminieren des Zustandes waehrend Hoare-Beweisen ***)
+(*** Bsp.: "!!s. s(Suc(0))=0 --> s(Suc(0))+1=1" wird zu "!!s b. b=0 --> b+1=1" ***)
+(**************************************************************************************************)
+
+(* pvars_of_term:term list (name:string,trm:term) gibt die Liste aller Programm-Variablen
+ aus trm zurueck. name gibt dabei den Namen der Zustandsvariablen an.
+ Bsp.: bei name="s" und dem Term "s(Suc(Suc(0)))=s(0)" (entspricht "c=a")
+ wird [0,Suc(Suc(0))] geliefert (Liste ist i.A. unsortiert) *)
+
+fun pvars_of_term (name,trm) =
+ let
+ fun add_vars (name,Free (s,t) $ trm,vl) =if name=s
+ then if trm mem vl
+ then vl
+ else trm::vl
+ else add_vars (name,trm,vl)
+ | add_vars (name,Abs (s,t,trm),vl) =add_vars (name,trm,vl)
+ | add_vars (name,trm1 $ trm2,vl) =add_vars (name,trm2,add_vars (name,trm1,vl))
+ | add_vars (_,_,vl) =vl
+ in
+ add_vars (name,trm,[])
+ end;
+
+(* VarsElimTac: Taktik zum Eliminieren von bestimmten Programmvariablen aus dem Subgoal i
+ - v::vl:(term) list Liste der zu eliminierenden Programmvariablen
+ - meta_spec:thm Theorem, welches zur Entfernung der Variablen benutzt wird
+ z.B.: "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))"
+ - namexAll:string Name von ^ (hier "x")
+ - varx:term Term zu ^ (hier Var(("x",0),...))
+ - varP:term Term zu ^ (hier Var(("P",0),...))
+ - type_pvar:typ Typ der Programmvariablen (d.h. 'a bei 'a prog, z.B.: nat, bool, ...)
+
+ Vorgehen:
+ - eliminiere jede pvar durch Anwendung von comp_inst_ren_tac. Dazu:
+ - Unbenennung in meta_spec: namexAll wird in den Namen der Prog.-Var. umbenannt
+ z.B.: fuer die Prog.-Var. mit Namen "a" ergibt sich
+ meta_spec zu "(!! s a.PROP P(s,a)) ==> (!! s.PROP P(s,x(s)))"
+ - Instanziierungen in meta_spec:
+ varx wird mit "%s:(type_pvar) state.s(pvar)" instanziiert
+ varP wird entsprechend instanziiert. Beispiel fuer Prog.-Var. "a":
+ - zu Subgoal "!!s.s(Suc(0)) = s(0) ==> s(0) = 1" bestimme Term ohne "!!s.":
+ trm0 = "s(Suc(0)) = s(0) ==> s(0) = 1" (s ist hier freie Variable)
+ - substituiere alle Vorkommen von s(pvar) durch eine freie Var. xs:
+ trm1 = "s(Suc(0)) = xs ==> xs = 1"
+ - abstrahiere ueber xs:
+ trm2 = "%xs.s(Suc(0)) = xs ==> xs = 1"
+ - abstrahiere ueber restliche Vorkommen von s:
+ trm3 = "%s xs.s(Suc(0)) = xs ==> xs = 1"
+ - instanziiere varP mit trm3
+*)
+
+fun VarsElimTac ([],_,_,_,_,_) i =all_tac
+ | VarsElimTac (v::vl,meta_spec,namexAll,varx,varP,type_pvar) i =
+ STATE (
+ fn state =>
+ comp_inst_ren_tac
+ [(namexAll,pvar2pvarID v)]
+ [(
+ cterm_of (#sign (rep_thm state)) varx,
+ cterm_of (#sign (rep_thm state)) (
+ Abs ("s",Type ("nat",[]) --> type_pvar,Bound 0 $ v)
+ )
+ ),(
+ cterm_of (#sign (rep_thm state)) varP,
+ cterm_of (#sign (rep_thm state)) (
+ let
+ val (_,_,_ $ Abs (_,_,trm),_) = dest_state (state,i);
+ val (sname,trm0) = variant_abs ("s",dummyT,trm);
+ val xsname = variant_name ("xs",trm0);
+ val trm1 = subst_term (Free (sname,dummyT) $ v,Syntax.free xsname,trm0)
+ val trm2 = Abs ("xs",type_pvar,abstract_over (Syntax.free xsname,trm1))
+ in
+ Abs ("s",Type ("nat",[]) --> type_pvar,abstract_over (Free (sname,dummyT),trm2))
+ end
+ )
+ )]
+ meta_spec i
+ )
+ THEN
+ (VarsElimTac (vl,meta_spec,namexAll,varx,varP,type_pvar) i);
+
+(* StateElimTac: Taktik zum Eliminieren aller Programmvariablen aus dem Subgoal i
+
+ zur Erinnerung:
+ - das Subgoal hat vor Anwendung dieser Taktik die Form "!!s:('a) state.P(s)",
+ d.h. den Term Const("all",_) $ Abs ("s",pvar --> 'a,_)
+ - meta_spec hat die Form "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))"
+*)
+
+fun StateElimTac i =
+ STATE (
+ fn state =>
+ let
+ val (_,_,_ $ Abs (_,Type ("fun",[_,type_pvar]),trm),_) = dest_state (state,i);
+ val _ $ (_ $ Abs (_,_,_ $ Abs (namexAll,_,_))) $
+ (_ $ Abs (_,_,varP $ _ $ (varx $ _))) = #prop (rep_thm meta_spec)
+ in
+ VarsElimTac (pvars_of_term (variant_abs ("s",dummyT,trm)),meta_spec,namexAll,varx,varP,type_pvar) i
+ end
+ );
+
+
+
+(*** tactics for verification condition generation ***)
+
+(* pre_cond:bool gibt an, ob das Subgoal von der Form Spec(?Q,c,p) ist oder nicht. Im Fall
+ von pre_cond=false besteht die Vorbedingung nur nur aus einer scheme-Variable. Die dann
+ generierte Verifikationsbedingung hat die Form "!!s.?Q --> ...". "?Q" kann deshalb zu gegebenen
+ Zeitpunkt mittels "rtac impI" und "atac" gebunden werden, die Bedingung loest sich dadurch auf. *)
+
+fun WlpTac i = (rtac SeqRule i) THEN (HoareRuleTac (i+1) false)
+and HoareRuleTac i pre_cond =
+ STATE(fn state =>
+ ((WlpTac i) THEN (HoareRuleTac i pre_cond))
+ ORELSE
+ (FIRST[rtac SkipRule i,
+ rtac AssignRule i,
+ EVERY[rtac IfRule i,
+ HoareRuleTac (i+2) false,
+ HoareRuleTac (i+1) false],
+ EVERY[rtac WhileRule i,
+ Asm_full_simp_tac (i+2),
+ HoareRuleTac (i+1) true]]
+ THEN
+ (if pre_cond then (Asm_full_simp_tac i) else (atac i))
+ )
+ );
+
+val HoareTac1 =
+ EVERY[HoareRuleTac 1 true, ALLGOALS StateElimTac, prune_params_tac];
+
+val hoare_tac = SELECT_GOAL (HoareTac1);
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/Hoare.thy Fri Nov 17 09:04:10 1995 +0100
@@ -0,0 +1,178 @@
+(* Title: HOL/Hoare/Hoare.thy
+ ID: $Id$
+ Author: Norbert Galm & Tobias Nipkow
+ Copyright 1995 TUM
+
+Sugared semantic embedding of Hoare logic.
+*)
+
+Hoare = Arith +
+
+types
+ 'a prog (* program syntax *)
+ pvar = "nat" (* encoding of program variables ( < 26! ) *)
+ 'a state = "pvar => 'a" (* program state *)
+ 'a exp ="'a state => 'a" (* denotation of expressions *)
+ 'a bexp = "'a state => bool" (* denotation of boolean expressions *)
+ 'a com = "'a state => 'a state => bool" (* denotation of programs *)
+
+syntax
+ "@Skip" :: "'a prog" ("SKIP")
+ "@Assign" :: "[id, 'a] => 'a prog" ("_ := _")
+ "@Seq" :: "['a prog, 'a prog] => 'a prog" ("_;//_" [0,1000] 999)
+ "@If" :: "[bool, 'a prog, 'a prog] => 'a prog"
+ ("IF _//THEN// (_)//ELSE// (_)//END")
+ "@While" :: "[bool, bool, 'a prog] => 'a prog"
+ ("WHILE _//DO {_}// (_)//END")
+
+ "@Spec" :: "[bool, 'a prog, bool] => bool" ("{_}//_//{_}")
+
+consts
+ (* semantics *)
+
+ Skip :: "'a com"
+ Assign :: "[pvar, 'a exp] => 'a com"
+ Seq :: "['a com, 'a com] => 'a com"
+ Cond :: "['a bexp, 'a com, 'a com] => 'a com"
+ While :: "['a bexp, 'a bexp, 'a com] => 'a com"
+ Iter :: "[nat, 'a bexp, 'a com] => 'a com"
+
+ Spec :: "['a bexp, 'a com, 'a bexp] => bool"
+
+defs
+ (* denotational semantics *)
+
+ SkipDef "Skip s s' == (s=s')"
+ AssignDef "Assign v e s s' == (s' = (%x.if x=v then e(s) else s(x)))"
+ SeqDef "Seq c c' s s' == ? s''. c s s'' & c' s'' s'"
+ CondDef "Cond b c c' s s' == (b(s) --> c s s') & (~b s --> c' s s')"
+ WhileDef "While b inv c s s' == ? n. Iter n b c s s'"
+
+ IterDef "Iter n b c == nat_rec n (%s s'.~b(s) & (s=s'))
+ (%n_rec iter_rec.%s s'.b(s) & Seq c iter_rec s s')"
+
+ SpecDef "Spec p c q == !s s'. c s s' --> p s --> q s'"
+
+end
+
+ML
+
+
+(*** term manipulation ***)
+
+(* name_in_term:bool (name:string,trm:term) bestimmt, ob in trm der Name name als Konstante,
+ freie Var., scheme-Variable oder als Name fuer eine Lambda-Abstraktion vorkommt *)
+
+fun name_in_term (name,Const (s,t)) =(name=s)
+ | name_in_term (name,Free (s,t)) =(name=s)
+ | name_in_term (name,Var ((s,i),t)) =(name=s ^ makestring i)
+ | name_in_term (name,Abs (s,t,trm)) =(name=s) orelse (name_in_term (name,trm))
+ | name_in_term (name,trm1 $ trm2) =(name_in_term (name,trm1)) orelse (name_in_term (name,trm2))
+ | name_in_term (_,_) =false;
+
+(* variant_name:string (name:string,trm:term) liefert einen von name abgewandelten Namen (durch Anhaengen
+ von genuegend vielen "_"), der nicht in trm vorkommt. Im Gegensatz zu variant_abs beruecktsichtigt es
+ auch Namen von scheme-Variablen und von Lambda-Abstraktionen in trm *)
+
+fun variant_name (name,trm) =if name_in_term (name,trm)
+ then variant_name (name ^ "_",trm)
+ else name;
+
+(* subst_term:term (von:term,nach:term,trm:term) liefert den Term, der aus
+trm entsteht, wenn alle Teilterme, die gleich von sind, durch nach ersetzt
+wurden *)
+
+fun subst_term (von,nach,Abs (s,t,trm)) =if von=Abs (s,t,trm)
+ then nach
+ else Abs (s,t,subst_term (von,nach,trm))
+ | subst_term (von,nach,trm1 $ trm2) =if von=trm1 $ trm2
+ then nach
+ else subst_term (von,nach,trm1) $ subst_term (von,nach,trm2)
+ | subst_term (von,nach,trm) =if von=trm
+ then nach
+ else trm;
+
+
+(* Translation between program vars ("a" - "z") and their encoding as
+ natural numbers: "a" <==> 0, "b" <==> Suc(0), ..., "z" <==> 25 *)
+
+fun is_pvarID s = size s=1 andalso "a"<=s andalso s<="z";
+
+fun pvarID2pvar s =
+ let fun rest2pvar (i,arg) =
+ if i=0 then arg else rest2pvar(i-1, Syntax.const "Suc" $ arg)
+ in rest2pvar(ord s - ord "a", Syntax.const "0") end;
+
+fun pvar2pvarID trm =
+ let
+ fun rest2pvarID (Const("0",_),i) =chr (i + ord "a")
+ | rest2pvarID (Const("Suc",_) $ trm,i) =rest2pvarID (trm,i+1)
+ in
+ rest2pvarID (trm,0)
+ end;
+
+
+(*** parse translations: syntax -> semantics ***)
+
+(* term_tr:term (name:string,trm:term) ersetzt in trm alle freien Variablen, die eine pvarID
+ darstellen, durch name $ pvarID2pvar(pvarID). Beispiel:
+ bei name="s" und dem Term "a=b & a=X" wird der Term "s(0)=s(Suc(0)) & s(0)=X" geliefert *)
+
+fun term_tr (name,Free (s,t)) = if is_pvarID s
+ then Syntax.free name $ pvarID2pvar s
+ else Free (s,t)
+ | term_tr (name,Abs (s,t,trm)) = Abs (s,t,term_tr (name,trm))
+ | term_tr (name,trm1 $ trm2) = term_tr (name,trm1) $ term_tr (name,trm2)
+ | term_tr (name,trm) = trm;
+
+fun bool_tr B =
+ let val name = variant_name("s",B)
+ in Abs (name,dummyT,abstract_over (Syntax.free name,term_tr (name,B))) end;
+
+fun exp_tr E =
+ let val name = variant_name("s",E)
+ in Abs (name,dummyT,abstract_over (Syntax.free name,term_tr (name,E))) end;
+
+fun prog_tr (Const ("@Skip",_)) = Syntax.const "Skip"
+ | prog_tr (Const ("@Assign",_) $ Free (V,_) $ E) =
+ if is_pvarID V
+ then Syntax.const "Assign" $ pvarID2pvar V $ exp_tr E
+ else error("Not a valid program variable: " ^ quote V)
+ | prog_tr (Const ("@Seq",_) $ C $ C') =
+ Syntax.const "Seq" $ prog_tr C $ prog_tr C'
+ | prog_tr (Const ("@If",_) $ B $ C $ C') =
+ Syntax.const "Cond" $ bool_tr B $ prog_tr C $ prog_tr C'
+ | prog_tr (Const ("@While",_) $ B $ INV $ C) =
+ Syntax.const "While" $ bool_tr B $ bool_tr INV $ prog_tr C;
+
+fun spec_tr [P,C,Q] = Syntax.const "Spec" $ bool_tr P $ prog_tr C $ bool_tr Q;
+
+val parse_translation = [("@Spec",spec_tr)];
+
+
+(*** print translations: semantics -> syntax ***)
+
+(* term_tr':term (name:string,trm:term) ersetzt in trm alle Vorkommen von name $ pvar durch
+ entsprechende freie Variablen, welche die pvarID zu pvar darstellen. Beispiel:
+ bei name="s" und dem Term "s(0)=s(Suc(0)) & s(0)=X" wird der Term "a=b & a=X" geliefert *)
+
+fun term_tr' (name,Free (s,t) $ trm) =if name=s
+ then Syntax.free (pvar2pvarID trm)
+ else Free (s,t) $ term_tr' (name,trm)
+ | term_tr' (name,Abs (s,t,trm)) =Abs (s,t,term_tr' (name,trm))
+ | term_tr' (name,trm1 $ trm2) =term_tr' (name,trm1) $ term_tr' (name,trm2)
+ | term_tr' (name,trm) =trm;
+
+fun bexp_tr' (Abs(_,_,b)) =term_tr' (variant_abs ("s",dummyT,b));
+
+fun exp_tr' (Abs(_,_,e)) =term_tr' (variant_abs ("s",dummyT,e));
+
+fun com_tr' (Const ("Skip",_)) =Syntax.const "@Skip"
+ | com_tr' (Const ("Assign",_) $ v $ e) =Syntax.const "@Assign" $ Syntax.free (pvar2pvarID v) $ exp_tr' e
+ | com_tr' (Const ("Seq",_) $ c $ c') =Syntax.const "@Seq" $ com_tr' c $ com_tr' c'
+ | com_tr' (Const ("Cond",_) $ b $ c $ c') =Syntax.const "@If" $ bexp_tr' b $ com_tr' c $ com_tr' c'
+ | com_tr' (Const ("While",_) $ b $ inv $ c) =Syntax.const "@While" $ bexp_tr' b $ bexp_tr' inv $ com_tr' c;
+
+fun spec_tr' [p,c,q] =Syntax.const "@Spec" $ bexp_tr' p $ com_tr' c $ bexp_tr' q;
+
+val print_translation =[("Spec",spec_tr')];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/README.html Fri Nov 17 09:04:10 1995 +0100
@@ -0,0 +1,36 @@
+<HTML><HEAD><TITLE>HOL/Hoare/ReadMe</TITLE></HEAD><BODY>
+
+<H2>Semantic Embedding of Hoare Logic</H2>
+
+This directory contains a sugared shallow semantic embedding of Hoare logic
+for a while language. The implementation closely follows<P>
+
+
+Mike Gordon.
+<cite>Mechanizing Programming Logics in Higher Order Logic.</cite><BR>
+University of Cambridge, Computer Laboratory, TR 145, 1988.<P>
+
+published as<P>
+
+Mike Gordon.
+<cite>Mechanizing Programming Logics in Higher Order Logic.</cite><BR>
+In
+<cite>Current Trends in Hardware Verification and Automated Theorem Proving
+</cite>,<BR>
+edited by G. Birtwistle and P.A. Subrahmanyam, Springer-Verlag, 1989.
+<P>
+
+At the top level, it provides a tactic <B>hoare_tac</B>, which transforms a
+goal
+<BLOCKQUOTE>
+<KBD>{P} prog {Q}</KBD>
+</BLOCKQUOTE>
+into a set of HOL-level verification conditions.
+<DL>
+<DT>Syntax:
+<DD> the letters a-z are interpreted as program variables,
+ all other identifiers as mathematical variables.<P>
+</DL>
+The pre/post conditions can be arbitrary HOL formulae including program
+variables. The program text should only refer to program variables.
+</BODY></HTML>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/ROOT.ML Fri Nov 17 09:04:10 1995 +0100
@@ -0,0 +1,12 @@
+(* Title: HOL/IMP/ROOT.ML
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 1995 TUM
+*)
+
+HOL_build_completed; (*Make examples fail if HOL did*)
+
+loadpath := ["Hoare"];
+use_thy "Examples";
+
+make_chart (); (*make HTML chart*)