--- a/src/HOLCF/ex/Hoare.ML Sun May 28 19:54:20 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,412 +0,0 @@
-(* Title: HOLCF/ex/hoare.ML
- ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-*)
-
-(* --------- pure HOLCF logic, some little lemmas ------ *)
-
-Goal "b~=TT ==> b=FF | b=UU";
-by (rtac (Exh_tr RS disjE) 1);
-by (fast_tac HOL_cs 1);
-by (etac disjE 1);
-by (contr_tac 1);
-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)";
-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";
-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";
-by (hyp_subst_tac 1);
-by (rtac hoare_lemma2 1);
-by (etac exE 1);
-by (etac LeastI 1);
-qed "hoare_lemma5";
-
-Goal "b=UU ==> b~=TT";
-by (hyp_subst_tac 1);
-by (resolve_tac dist_eq_tr 1);
-qed "hoare_lemma6";
-
-Goal "b=FF ==> b~=TT";
-by (hyp_subst_tac 1);
-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";
-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 (atac 2);
-by (rtac (le_less_trans RS less_irrefl) 1);
-by (atac 2);
-by (rtac Least_le 1);
-by (etac hoare_lemma6 1);
-by (rtac (le_less_trans RS less_irrefl) 1);
-by (atac 2);
-by (rtac Least_le 1);
-by (etac hoare_lemma7 1);
-qed "hoare_lemma8";
-
-
-Goal "f$(y::'a)=(UU::tr) ==> f$UU = UU";
-by (etac (flat_codom RS disjE) 1);
-by Auto_tac;
-qed "hoare_lemma28";
-
-
-(* ----- access to definitions ----- *)
-
-Goal "p$x = If b1$x then p$(g$x) else x fi";
-by (fix_tac3 p_def 1);
-by (Simp_tac 1);
-qed "p_def3";
-
-Goal "q$x = If b1$x orelse b2$x then q$(g$x) else x fi";
-by (fix_tac3 q_def 1);
-by (Simp_tac 1);
-qed "q_def3";
-
-(** --------- 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";
-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 (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 (rtac mp 1);
-by (etac spec 1);
-by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
-by (simp_tac HOLCF_ss 1);
-by (etac mp 1);
-by (strip_tac 1);
-by (rtac mp 1);
-by (etac spec 1);
-by (etac less_trans 1);
-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";
-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 (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 (fast_tac HOL_cs 1);
-by (simp_tac HOLCF_ss 1);
-by (etac mp 1);
-by (strip_tac 1);
-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) ------- *)
-
-
-val hoare_lemma10 = (hoare_lemma8 RS (hoare_lemma9 RS mp));
-(*
-val hoare_lemma10 = "[| EX k. b1$(iterate k g ?x1) ~= TT;
- Suc ?k3 = Least(%n. b1$(iterate n g ?x1) ~= TT) |] ==>
- p$(iterate ?k3 g ?x1) = p$?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 \
-\ --> p$x = iterate k$g$x";
-by (case_tac "k" 1);
-by (hyp_subst_tac 1);
-by (Simp_tac 1);
-by (strip_tac 1);
-by (etac conjE 1);
-by (rtac trans 1);
-by (rtac p_def3 1);
-by (asm_simp_tac HOLCF_ss 1);
-by (hyp_subst_tac 1);
-by (strip_tac 1);
-by (etac conjE 1);
-by (rtac trans 1);
-by (etac (hoare_lemma10 RS sym) 1);
-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 (rtac (hoare_lemma8 RS spec RS mp) 1);
-by (atac 1);
-by (atac 1);
-by (Simp_tac 1);
-by (simp_tac HOLCF_ss 1);
-by (rtac trans 1);
-by (rtac p_def3 1);
-by (simp_tac (simpset() delsimps [iterate_Suc] addsimps [iterate_Suc RS sym]) 1);
-by (eres_inst_tac [("s","FF")] ssubst 1);
-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 \
-\ --> p$x = UU";
-by (case_tac "k" 1);
-by (hyp_subst_tac 1);
-by (Simp_tac 1);
-by (strip_tac 1);
-by (etac conjE 1);
-by (rtac trans 1);
-by (rtac p_def3 1);
-by (asm_simp_tac HOLCF_ss 1);
-by (hyp_subst_tac 1);
-by (Simp_tac 1);
-by (strip_tac 1);
-by (etac conjE 1);
-by (rtac trans 1);
-by (rtac (hoare_lemma10 RS sym) 1);
-by (atac 1);
-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 (rtac (hoare_lemma8 RS spec RS mp) 1);
-by (atac 1);
-by (atac 1);
-by (Simp_tac 1);
-by (asm_simp_tac HOLCF_ss 1);
-by (rtac trans 1);
-by (rtac p_def3 1);
-by (asm_simp_tac HOLCF_ss 1);
-qed "hoare_lemma12";
-
-(* -------- 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";
-by (rtac (p_def RS def_fix_ind) 1);
-by (rtac adm_all 1);
-by (rtac allI 1);
-by (rtac adm_eq 1);
-by (cont_tacR 1);
-by (rtac allI 1);
-by (stac Rep_CFun_strict1 1);
-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 (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";
-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) ------- *)
-
-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);
-by (rtac adm_eq 1);
-by (cont_tacR 1);
-by (rtac allI 1);
-by (stac Rep_CFun_strict1 1);
-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 (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";
-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)";
-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";
-by (rtac (q_def RS def_fix_ind) 1);
-by (rtac adm_all 1);
-by (rtac allI 1);
-by (rtac adm_eq 1);
-by (cont_tacR 1);
-by (rtac allI 1);
-by (stac Rep_CFun_strict1 1);
-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 (etac spec 1);
-by (asm_simp_tac HOLCF_ss 1);
-by (rtac (iterate_Suc RS subst) 1);
-by (etac spec 1);
-qed "hoare_lemma20";
-
-Goal "(ALL y. b1$(y::'a)=TT) ==> q$(x::'a) = UU";
-by (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1);
-by (etac (hoare_lemma20 RS spec) 1);
-qed "hoare_lemma21";
-
-Goal "b1$(UU::'a)=UU ==> q$(UU::'a) = UU";
-by (stac q_def3 1);
-by (asm_simp_tac HOLCF_ss 1);
-qed "hoare_lemma22";
-
-(* -------- results about q for case (EX k. b1$(iterate k$g$x) ~= TT) ------- *)
-
-val hoare_lemma25 = (hoare_lemma8 RS (hoare_lemma24 RS mp) );
-(*
-val hoare_lemma25 = "[| EX k. b1$(iterate k g ?x1) ~= TT;
- Suc ?k3 = Least(%n. b1$(iterate n g ?x1) ~= TT) |] ==>
- 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)";
-by (case_tac "k" 1);
-by (hyp_subst_tac 1);
-by (strip_tac 1);
-by (Simp_tac 1);
-by (hyp_subst_tac 1);
-by (strip_tac 1);
-by (etac conjE 1);
-by (rtac trans 1);
-by (rtac (hoare_lemma25 RS sym) 1);
-by (atac 1);
-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 (rtac (hoare_lemma8 RS spec RS mp) 1);
-by (atac 1);
-by (atac 1);
-by (Simp_tac 1);
-by (simp_tac HOLCF_ss 1);
-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 \
-\ --> q$x = UU";
-by (case_tac "k" 1);
-by (hyp_subst_tac 1);
-by (Simp_tac 1);
-by (strip_tac 1);
-by (etac conjE 1);
-by (stac q_def3 1);
-by (asm_simp_tac HOLCF_ss 1);
-by (hyp_subst_tac 1);
-by (Simp_tac 1);
-by (strip_tac 1);
-by (etac conjE 1);
-by (rtac trans 1);
-by (rtac (hoare_lemma25 RS sym) 1);
-by (atac 1);
-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 (rtac (hoare_lemma8 RS spec RS mp) 1);
-by (atac 1);
-by (atac 1);
-by (Simp_tac 1);
-by (asm_simp_tac HOLCF_ss 1);
-by (rtac trans 1);
-by (rtac q_def3 1);
-by (asm_simp_tac HOLCF_ss 1);
-qed "hoare_lemma27";
-
-(* ------- (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";
-by (stac hoare_lemma16 1);
-by (atac 1);
-by (rtac (hoare_lemma19 RS disjE) 1);
-by (atac 1);
-by (stac hoare_lemma18 1);
-by (atac 1);
-by (stac hoare_lemma22 1);
-by (atac 1);
-by (rtac refl 1);
-by (stac hoare_lemma21 1);
-by (atac 1);
-by (stac hoare_lemma21 1);
-by (atac 1);
-by (rtac refl 1);
-qed "hoare_lemma23";
-
-(* ------------ 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";
-by (rtac (hoare_lemma5 RS disjE) 1);
-by (atac 1);
-by (rtac refl 1);
-by (stac (hoare_lemma11 RS mp) 1);
-by (atac 1);
-by (rtac conjI 1);
-by (rtac refl 1);
-by (atac 1);
-by (rtac (hoare_lemma26 RS mp RS subst) 1);
-by (atac 1);
-by (rtac conjI 1);
-by (rtac refl 1);
-by (atac 1);
-by (rtac refl 1);
-by (stac (hoare_lemma12 RS mp) 1);
-by (atac 1);
-by (rtac conjI 1);
-by (rtac refl 1);
-by (atac 1);
-by (stac hoare_lemma22 1);
-by (stac hoare_lemma28 1);
-by (atac 1);
-by (rtac refl 1);
-by (rtac sym 1);
-by (stac (hoare_lemma27 RS mp) 1);
-by (atac 1);
-by (rtac conjI 1);
-by (rtac refl 1);
-by (atac 1);
-by (rtac refl 1);
-qed "hoare_lemma29";
-
-(* ------ the main prove q o p = q ------ *)
-
-Goal "q oo p = q";
-by (rtac ext_cfun 1);
-by (stac cfcomp2 1);
-by (rtac (hoare_lemma3 RS disjE) 1);
-by (etac hoare_lemma23 1);
-by (etac hoare_lemma29 1);
-qed "hoare_main";