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/ex/Hoare.ML
changeset 18075 43000d7a017c
parent 17291 94f6113fe9ed 
--- a/src/HOLCF/ex/Hoare.ML	Thu Nov 03 00:43:11 2005 +0100
+++ b/src/HOLCF/ex/Hoare.ML	Thu Nov 03 00:43:50 2005 +0100
@@ -14,21 +14,21 @@
 by (fast_tac HOL_cs 1);
 qed "hoare_lemma2";
 
-Goal " (ALL k. b1$(iterate k g x) = TT) | (EX k. b1$(iterate k g x)~=TT)";
+Goal " (ALL k. b1$(iterate k$g$x) = TT) | (EX k. b1$(iterate k$g$x)~=TT)";
 by (fast_tac HOL_cs 1);
 qed "hoare_lemma3";
 
-Goal "(EX k. b1$(iterate k g x) ~= TT) ==> \
-\ EX k. b1$(iterate k g x) = FF | b1$(iterate k g x) = UU";
+Goal "(EX k. b1$(iterate k$g$x) ~= TT) ==> \
+\ EX k. b1$(iterate k$g$x) = FF | b1$(iterate k$g$x) = UU";
 by (etac exE 1);
 by (rtac exI 1);
 by (rtac hoare_lemma2 1);
 by (atac 1);
 qed "hoare_lemma4";
 
-Goal "[|(EX k. b1$(iterate k g x) ~= TT);\
-\   k=Least(%n. b1$(iterate n g x) ~= TT)|] ==> \
-\ b1$(iterate k g x)=FF | b1$(iterate k g x)=UU";
+Goal "[|(EX k. b1$(iterate k$g$x) ~= TT);\
+\   k=Least(%n. b1$(iterate n$g$x) ~= TT)|] ==> \
+\ b1$(iterate k$g$x)=FF | b1$(iterate k$g$x)=UU";
 by (hyp_subst_tac 1);
 by (rtac hoare_lemma2 1);
 by (etac exE 1);
@@ -45,13 +45,13 @@
 by (resolve_tac dist_eq_tr 1);
 qed "hoare_lemma7";
 
-Goal "[|(EX k. b1$(iterate k g x) ~= TT);\
-\   k=Least(%n. b1$(iterate n g x) ~= TT)|] ==> \
-\ ALL m. m < k --> b1$(iterate m g x)=TT";
+Goal "[|(EX k. b1$(iterate k$g$x) ~= TT);\
+\   k=Least(%n. b1$(iterate n$g$x) ~= TT)|] ==> \
+\ ALL m. m < k --> b1$(iterate m$g$x)=TT";
 by (hyp_subst_tac 1);
 by (etac exE 1);
 by (strip_tac 1);
-by (res_inst_tac [("p","b1$(iterate m g x)")] trE 1);
+by (res_inst_tac [("p","b1$(iterate m$g$x)")] trE 1);
 by (atac 2);
 by (rtac (le_less_trans RS less_irrefl) 1);
 by (atac 2);
@@ -84,16 +84,16 @@
 
 (** --------- proves about iterations of p and q ---------- **)
 
-Goal "(ALL m. m< Suc k --> b1$(iterate m g x)=TT) -->\
-\  p$(iterate k g x)=p$x";
+Goal "(ALL m. m< Suc k --> b1$(iterate m$g$x)=TT) -->\
+\  p$(iterate k$g$x)=p$x";
 by (induct_tac "k" 1);
 by (Simp_tac 1);
 by (Simp_tac 1);
 by (strip_tac 1);
-by (res_inst_tac [("s","p$(iterate n g x)")] trans 1);
+by (res_inst_tac [("s","p$(iterate n$g$x)")] trans 1);
 by (rtac trans 1);
 by (rtac (p_def3 RS sym) 2);
-by (res_inst_tac [("s","TT"),("t","b1$(iterate n g x)")] ssubst 1);
+by (res_inst_tac [("s","TT"),("t","b1$(iterate n$g$x)")] ssubst 1);
 by (rtac mp 1);
 by (etac spec 1);
 by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
@@ -106,16 +106,16 @@
 by (Simp_tac 1);
 qed "hoare_lemma9";
 
-Goal "(ALL m. m< Suc k --> b1$(iterate m g x)=TT) --> \
-\ q$(iterate k g x)=q$x";
+Goal "(ALL m. m< Suc k --> b1$(iterate m$g$x)=TT) --> \
+\ q$(iterate k$g$x)=q$x";
 by (induct_tac "k" 1);
 by (Simp_tac 1);
 by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
 by (strip_tac 1);
-by (res_inst_tac [("s","q$(iterate n g x)")] trans 1);
+by (res_inst_tac [("s","q$(iterate n$g$x)")] trans 1);
 by (rtac trans 1);
 by (rtac (q_def3 RS sym) 2);
-by (res_inst_tac [("s","TT"),("t","b1$(iterate n g x)")] ssubst 1);
+by (res_inst_tac [("s","TT"),("t","b1$(iterate n$g$x)")] ssubst 1);
 by (fast_tac HOL_cs 1);
 by (simp_tac HOLCF_ss 1);
 by (etac mp 1);
@@ -123,7 +123,7 @@
 by (fast_tac (HOL_cs addSDs [less_Suc_eq RS iffD1]) 1);
 qed "hoare_lemma24";
 
-(* -------- results about p for case (EX k. b1$(iterate k g x)~=TT) ------- *)
+(* -------- results about p for case (EX k. b1$(iterate k$g$x)~=TT) ------- *)
 
 
 val hoare_lemma10 = (hoare_lemma8 RS (hoare_lemma9 RS mp));
@@ -134,9 +134,9 @@
 
 *)
 
-Goal "(EX n. b1$(iterate n g x) ~= TT) ==>\
-\ k=(LEAST n. b1$(iterate n g x) ~= TT) & b1$(iterate k g x)=FF \
-\ --> p$x = iterate k g x";
+Goal "(EX n. b1$(iterate n$g$x) ~= TT) ==>\
+\ k=(LEAST n. b1$(iterate n$g$x) ~= TT) & b1$(iterate k$g$x)=FF \
+\ --> p$x = iterate k$g$x";
 by (case_tac "k" 1);
 by (hyp_subst_tac 1);
 by (Simp_tac 1);
@@ -153,7 +153,7 @@
 by (atac 1);
 by (rtac trans 1);
 by (rtac p_def3 1);
-by (res_inst_tac [("s","TT"),("t","b1$(iterate nat g x)")] ssubst 1);
+by (res_inst_tac [("s","TT"),("t","b1$(iterate nat$g$x)")] ssubst 1);
 by (rtac (hoare_lemma8 RS spec RS mp) 1);
 by (atac 1);
 by (atac 1);
@@ -166,8 +166,8 @@
 by (simp_tac HOLCF_ss 1);
 qed "hoare_lemma11";
 
-Goal "(EX n. b1$(iterate n g x) ~= TT) ==>\
-\ k=Least(%n. b1$(iterate n g x)~=TT) & b1$(iterate k g x)=UU \
+Goal "(EX n. b1$(iterate n$g$x) ~= TT) ==>\
+\ k=Least(%n. b1$(iterate n$g$x)~=TT) & b1$(iterate k$g$x)=UU \
 \ --> p$x = UU";
 by (case_tac "k" 1);
 by (hyp_subst_tac 1);
@@ -187,7 +187,7 @@
 by (atac 1);
 by (rtac trans 1);
 by (rtac p_def3 1);
-by (res_inst_tac [("s","TT"),("t","b1$(iterate nat g x)")] ssubst 1);
+by (res_inst_tac [("s","TT"),("t","b1$(iterate nat$g$x)")] ssubst 1);
 by (rtac (hoare_lemma8 RS spec RS mp) 1);
 by (atac 1);
 by (atac 1);
@@ -198,9 +198,9 @@
 by (asm_simp_tac HOLCF_ss 1);
 qed "hoare_lemma12";
 
-(* -------- results about p for case  (ALL k. b1$(iterate k g x)=TT) ------- *)
+(* -------- results about p for case  (ALL k. b1$(iterate k$g$x)=TT) ------- *)
 
-Goal "(ALL k. b1$(iterate k g x)=TT) ==> ALL k. p$(iterate k g x) = UU";
+Goal "(ALL k. b1$(iterate k$g$x)=TT) ==> ALL k. p$(iterate k$g$x) = UU";
 by (rtac (p_def RS def_fix_ind) 1);
 by (rtac adm_all 1);
 by (rtac allI 1);
@@ -211,21 +211,21 @@
 by (rtac refl 1);
 by (Simp_tac 1);
 by (rtac allI 1);
-by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1);
+by (res_inst_tac [("s","TT"),("t","b1$(iterate k$g$x)")] ssubst 1);
 by (etac spec 1);
 by (asm_simp_tac HOLCF_ss 1);
 by (rtac (iterate_Suc RS subst) 1);
 by (etac spec 1);
 qed "fernpass_lemma";
 
-Goal "(ALL k. b1$(iterate k g x)=TT) ==> p$x = UU";
+Goal "(ALL k. b1$(iterate k$g$x)=TT) ==> p$x = UU";
 by (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1);
 by (etac (fernpass_lemma RS spec) 1);
 qed "hoare_lemma16";
 
-(* -------- results about q for case  (ALL k. b1$(iterate k g x)=TT) ------- *)
+(* -------- results about q for case  (ALL k. b1$(iterate k$g$x)=TT) ------- *)
 
-Goal "(ALL k. b1$(iterate k g x)=TT) ==> ALL k. q$(iterate k g x) = UU";
+Goal "(ALL k. b1$(iterate k$g$x)=TT) ==> ALL k. q$(iterate k$g$x) = UU";
 by (rtac (q_def RS def_fix_ind) 1);
 by (rtac adm_all 1);
 by (rtac allI 1);
@@ -236,25 +236,25 @@
 by (rtac refl 1);
 by (rtac allI 1);
 by (Simp_tac 1);
-by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1);
+by (res_inst_tac [("s","TT"),("t","b1$(iterate k$g$x)")] ssubst 1);
 by (etac spec 1);
 by (asm_simp_tac HOLCF_ss 1);
 by (rtac (iterate_Suc RS subst) 1);
 by (etac spec 1);
 qed "hoare_lemma17";
 
-Goal "(ALL k. b1$(iterate k g x)=TT) ==> q$x = UU";
+Goal "(ALL k. b1$(iterate k$g$x)=TT) ==> q$x = UU";
 by (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1);
 by (etac (hoare_lemma17 RS spec) 1);
 qed "hoare_lemma18";
 
-Goal "(ALL k. (b1::'a->tr)$(iterate k g x)=TT) ==> b1$(UU::'a) = UU | (ALL y. b1$(y::'a)=TT)";
+Goal "(ALL k. (b1::'a->tr)$(iterate k$g$x)=TT) ==> b1$(UU::'a) = UU | (ALL y. b1$(y::'a)=TT)";
 by (rtac (flat_codom) 1);
 by (res_inst_tac [("t","x1")] (iterate_0 RS subst) 1);
 by (etac spec 1);
 qed "hoare_lemma19";
 
-Goal "(ALL y. b1$(y::'a)=TT) ==> ALL k. q$(iterate k g (x::'a)) = UU";
+Goal "(ALL y. b1$(y::'a)=TT) ==> ALL k. q$(iterate k$g$(x::'a)) = UU";
 by (rtac (q_def RS def_fix_ind) 1);
 by (rtac adm_all 1);
 by (rtac allI 1);
@@ -265,7 +265,7 @@
 by (rtac refl 1);
 by (rtac allI 1);
 by (Simp_tac 1);
-by (res_inst_tac [("s","TT"),("t","b1$(iterate k g (x::'a))")] ssubst 1);
+by (res_inst_tac [("s","TT"),("t","b1$(iterate k$g$(x::'a))")] ssubst 1);
 by (etac spec 1);
 by (asm_simp_tac HOLCF_ss 1);
 by (rtac (iterate_Suc RS subst) 1);
@@ -282,7 +282,7 @@
 by (asm_simp_tac HOLCF_ss 1);
 qed "hoare_lemma22";
 
-(* -------- results about q for case (EX k. b1$(iterate k g x) ~= TT) ------- *)
+(* -------- results about q for case (EX k. b1$(iterate k$g$x) ~= TT) ------- *)
 
 val hoare_lemma25 = (hoare_lemma8 RS (hoare_lemma24 RS mp) );
 (*
@@ -291,9 +291,9 @@
  q$(iterate ?k3 g ?x1) = q$?x1" : thm
 *)
 
-Goal "(EX n. b1$(iterate n g x)~=TT) ==>\
-\ k=Least(%n. b1$(iterate n g x) ~= TT) & b1$(iterate k g x) =FF \
-\ --> q$x = q$(iterate k g x)";
+Goal "(EX n. b1$(iterate n$g$x)~=TT) ==>\
+\ k=Least(%n. b1$(iterate n$g$x) ~= TT) & b1$(iterate k$g$x) =FF \
+\ --> q$x = q$(iterate k$g$x)";
 by (case_tac "k" 1);
 by (hyp_subst_tac 1);
 by (strip_tac 1);
@@ -307,7 +307,7 @@
 by (atac 1);
 by (rtac trans 1);
 by (rtac q_def3 1);
-by (res_inst_tac [("s","TT"),("t","b1$(iterate nat g x)")] ssubst 1);
+by (res_inst_tac [("s","TT"),("t","b1$(iterate nat$g$x)")] ssubst 1);
 by (rtac (hoare_lemma8 RS spec RS mp) 1);
 by (atac 1);
 by (atac 1);
@@ -316,8 +316,8 @@
 qed "hoare_lemma26";
 
 
-Goal "(EX n. b1$(iterate n g x) ~= TT) ==>\
-\ k=Least(%n. b1$(iterate n g x)~=TT) & b1$(iterate k g x)=UU \
+Goal "(EX n. b1$(iterate n$g$x) ~= TT) ==>\
+\ k=Least(%n. b1$(iterate n$g$x)~=TT) & b1$(iterate k$g$x)=UU \
 \ --> q$x = UU";
 by (case_tac "k" 1);
 by (hyp_subst_tac 1);
@@ -336,7 +336,7 @@
 by (atac 1);
 by (rtac trans 1);
 by (rtac q_def3 1);
-by (res_inst_tac [("s","TT"),("t","b1$(iterate nat g x)")] ssubst 1);
+by (res_inst_tac [("s","TT"),("t","b1$(iterate nat$g$x)")] ssubst 1);
 by (rtac (hoare_lemma8 RS spec RS mp) 1);
 by (atac 1);
 by (atac 1);
@@ -347,9 +347,9 @@
 by (asm_simp_tac HOLCF_ss 1);
 qed "hoare_lemma27";
 
-(* ------- (ALL k. b1$(iterate k g x)=TT) ==> q o p = q   ----- *)
+(* ------- (ALL k. b1$(iterate k$g$x)=TT) ==> q o p = q   ----- *)
 
-Goal "(ALL k. b1$(iterate k g x)=TT) ==> q$(p$x) = q$x";
+Goal "(ALL k. b1$(iterate k$g$x)=TT) ==> q$(p$x) = q$x";
 by (stac hoare_lemma16 1);
 by (atac 1);
 by (rtac (hoare_lemma19 RS disjE) 1);
@@ -366,9 +366,9 @@
 by (rtac refl 1);
 qed "hoare_lemma23";
 
-(* ------------  EX k. b1~(iterate k g x) ~= TT ==> q o p = q   ----- *)
+(* ------------  EX k. b1~(iterate k$g$x) ~= TT ==> q o p = q   ----- *)
 
-Goal "EX k. b1$(iterate k g x) ~= TT ==> q$(p$x) = q$x";
+Goal "EX k. b1$(iterate k$g$x) ~= TT ==> q$(p$x) = q$x";
 by (rtac (hoare_lemma5 RS disjE) 1);
 by (atac 1);
 by (rtac refl 1);
isabelle