# HG changeset patch # User wenzelm # Date 894628485 -7200 # Node ID be73ddff6c5a357e9b0ed8f138d5b4584ed03324 # Parent 5f6b2dd1cd11d601211c0e257ac5f1ebc5d2802f proper thy files; diff -r 5f6b2dd1cd11 -r be73ddff6c5a src/LCF/IsaMakefile --- a/src/LCF/IsaMakefile Fri May 08 10:15:39 1998 +0200 +++ b/src/LCF/IsaMakefile Fri May 08 13:54:45 1998 +0200 @@ -26,7 +26,8 @@ FOL: @cd $(SRC)/FOL; $(ISATOOL) make FOL -$(OUT)/LCF: $(OUT)/FOL LCF.ML LCF.thy ROOT.ML fix.ML pair.ML simpdata.ML +$(OUT)/LCF: $(OUT)/FOL LCF.ML LCF.thy ROOT.ML fix.ML fix.thy pair.ML \ + pair.thy simpdata.ML @$(ISATOOL) usedir -b $(OUT)/FOL LCF @@ -34,7 +35,8 @@ LCF-ex: LCF $(LOG)/LCF-ex.gz -$(LOG)/LCF-ex.gz: $(OUT)/LCF ex/ROOT.ML ex/ex.ML +$(LOG)/LCF-ex.gz: $(OUT)/LCF ex/Ex1.ML ex/Ex1.thy ex/Ex2.ML ex/Ex2.thy \ + ex/Ex3.ML ex/Ex3.thy ex/Ex4.ML ex/Ex4.thy ex/ROOT.ML @$(ISATOOL) usedir $(OUT)/LCF ex diff -r 5f6b2dd1cd11 -r be73ddff6c5a src/LCF/ROOT.ML --- a/src/LCF/ROOT.ML Fri May 08 10:15:39 1998 +0200 +++ b/src/LCF/ROOT.ML Fri May 08 13:54:45 1998 +0200 @@ -14,7 +14,7 @@ print_depth 1; use_thy "LCF"; use"simpdata.ML"; -use"pair.ML"; -use"fix.ML"; +use_thy"pair"; +use_thy"fix"; val LCF_build_completed = (); (*indicate successful build*) diff -r 5f6b2dd1cd11 -r be73ddff6c5a src/LCF/ex/Ex1.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/LCF/ex/Ex1.ML Fri May 08 13:54:45 1998 +0200 @@ -0,0 +1,28 @@ + +simpset_ref() := LCF_ss; + +Addsimps [P_strict,K]; + +val H_unfold = prove_goal thy "H = K(H)" + (fn _ => [stac H 1, rtac (FIX_eq RS sym) 1]); + +bind_thm ("H_unfold", H_unfold); + + +val H_strict = prove_goal thy "H(UU)=UU" + (fn _ => [stac H_unfold 1, Simp_tac 1]); + +bind_thm ("H_strict", H_strict); +Addsimps [H_strict]; + +goal thy "ALL x. H(FIX(K,x)) = FIX(K,x)"; +by (induct_tac "K" 1); +by (Simp_tac 1); +by (simp_tac (simpset() setloop (split_tac [COND_cases_iff])) 1); +by (strip_tac 1); +by (stac H_unfold 1); +by (Asm_simp_tac 1); +qed "H_idemp_lemma"; + +val H_idemp = rewrite_rule [mk_meta_eq (H RS sym)] H_idemp_lemma; +bind_thm ("H_idemp", H_idemp); diff -r 5f6b2dd1cd11 -r be73ddff6c5a src/LCF/ex/Ex1.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/LCF/ex/Ex1.thy Fri May 08 13:54:45 1998 +0200 @@ -0,0 +1,17 @@ + +(*** Section 10.4 ***) + +Ex1 = LCF + + +consts + P :: "'a => tr" + G :: "'a => 'a" + H :: "'a => 'a" + K :: "('a => 'a) => ('a => 'a)" + +rules + P_strict "P(UU) = UU" + K "K = (%h x. P(x) => x | h(h(G(x))))" + H "H = FIX(K)" + +end diff -r 5f6b2dd1cd11 -r be73ddff6c5a src/LCF/ex/Ex2.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/LCF/ex/Ex2.ML Fri May 08 13:54:45 1998 +0200 @@ -0,0 +1,11 @@ + +simpset_ref() := LCF_ss; + +Addsimps [F_strict,K]; + +goal thy "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))"; +by (stac H 1); +by (induct_tac "K::('a=>'b=>'b)=>('a=>'b=>'b)" 1); +by (Simp_tac 1); +by (asm_simp_tac (simpset() setloop (split_tac [COND_cases_iff])) 1); +qed "example"; diff -r 5f6b2dd1cd11 -r be73ddff6c5a src/LCF/ex/Ex2.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/LCF/ex/Ex2.thy Fri May 08 13:54:45 1998 +0200 @@ -0,0 +1,18 @@ + +(*** Example 3.8 ***) + +Ex2 = LCF + + +consts + P :: "'a => tr" + F :: "'a => 'a" + G :: "'a => 'a" + H :: "'a => 'b => 'b" + K :: "('a => 'b => 'b) => ('a => 'b => 'b)" + +rules + F_strict "F(UU) = UU" + K "K = (%h x y. P(x) => y | F(h(G(x),y)))" + H "H = FIX(K)" + +end diff -r 5f6b2dd1cd11 -r be73ddff6c5a src/LCF/ex/Ex3.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/LCF/ex/Ex3.ML Fri May 08 13:54:45 1998 +0200 @@ -0,0 +1,11 @@ + +simpset_ref() := LCF_ss; + +Addsimps [p_strict,p_s]; + +goal thy "p(FIX(s),y) = FIX(s)"; +by (induct_tac "s" 1); +by (Simp_tac 1); +by (Simp_tac 1); +qed "example"; + diff -r 5f6b2dd1cd11 -r be73ddff6c5a src/LCF/ex/Ex3.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/LCF/ex/Ex3.thy Fri May 08 13:54:45 1998 +0200 @@ -0,0 +1,14 @@ + +(*** Addition with fixpoint of successor ***) + +Ex3 = LCF + + +consts + s :: "'a => 'a" + p :: "'a => 'a => 'a" + +rules + p_strict "p(UU) = UU" + p_s "p(s(x),y) = s(p(x,y))" + +end diff -r 5f6b2dd1cd11 -r be73ddff6c5a src/LCF/ex/Ex4.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/LCF/ex/Ex4.ML Fri May 08 13:54:45 1998 +0200 @@ -0,0 +1,13 @@ + +val asms = goal thy "[| f(p) << p; !!q. f(q) << q ==> p << q |] ==> FIX(f)=p"; +by (rewtac eq_def); +by (rtac conjI 1); +by (induct_tac "f" 1); +by (rtac minimal 1); +by (strip_tac 1); +by (rtac less_trans 1); +by (resolve_tac asms 2); +by (etac less_ap_term 1); +by (resolve_tac asms 1); +by (rtac (FIX_eq RS eq_imp_less1) 1); +qed "example"; diff -r 5f6b2dd1cd11 -r be73ddff6c5a src/LCF/ex/Ex4.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/LCF/ex/Ex4.thy Fri May 08 13:54:45 1998 +0200 @@ -0,0 +1,4 @@ + +(*** Prefixpoints ***) + +Ex4 = LCF diff -r 5f6b2dd1cd11 -r be73ddff6c5a src/LCF/ex/ROOT.ML --- a/src/LCF/ex/ROOT.ML Fri May 08 10:15:39 1998 +0200 +++ b/src/LCF/ex/ROOT.ML Fri May 08 13:54:45 1998 +0200 @@ -1,7 +1,17 @@ +(* Title: LCF/ex/ROOT.ML + ID: $Id$ + Author: Tobias Nipkow + Copyright 1991 University of Cambridge + +Some examples from Lawrence Paulson's book Logic and Computation. +*) writeln"Root file for LCF examples"; LCF_build_completed; (*Cause examples to fail if LCF did*) set proof_timing; -use "ex.ML"; +use_thy "Ex1"; +use_thy "Ex2"; +use_thy "Ex3"; +use_thy "Ex4"; diff -r 5f6b2dd1cd11 -r be73ddff6c5a src/LCF/ex/ex.ML --- a/src/LCF/ex/ex.ML Fri May 08 10:15:39 1998 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,128 +0,0 @@ -(* Title: LCF/ex/ex.ML - ID: $Id$ - Author: Tobias Nipkow - Copyright 1991 University of Cambridge - -Some examples from Lawrence Paulson's book Logic and Computation. -*) - - -val add_axioms = PureThy.add_axioms o map Attribute.none; - - -(*** Section 10.4 ***) - -val ex_thy = - thy - |> Theory.add_consts - [("P", "'a => tr", NoSyn), - ("G", "'a => 'a", NoSyn), - ("H", "'a => 'a", NoSyn), - ("K", "('a => 'a) => ('a => 'a)", NoSyn)] - |> add_axioms - [("P_strict", "P(UU) = UU"), - ("K", "K = (%h x. P(x) => x | h(h(G(x))))"), - ("H", "H = FIX(K)")] - |> Theory.add_name "Ex 10.4"; - -val ax = get_axiom ex_thy; - -val P_strict = ax"P_strict"; -val K = ax"K"; -val H = ax"H"; - -val ex_ss = LCF_ss addsimps [P_strict,K]; - - -val H_unfold = prove_goal ex_thy "H = K(H)" - (fn _ => [stac H 1, rtac (FIX_eq RS sym) 1]); - -val H_strict = prove_goal ex_thy "H(UU)=UU" - (fn _ => [stac H_unfold 1, simp_tac ex_ss 1]); - -val ex_ss = ex_ss addsimps [H_strict]; - -goal ex_thy "ALL x. H(FIX(K,x)) = FIX(K,x)"; -by (induct_tac "K" 1); -by (simp_tac ex_ss 1); -by (simp_tac (ex_ss setloop (split_tac [COND_cases_iff])) 1); -by (strip_tac 1); -by (stac H_unfold 1); -by (asm_simp_tac ex_ss 1); -val H_idemp_lemma = topthm(); - -val H_idemp = rewrite_rule [mk_meta_eq (H RS sym)] H_idemp_lemma; - - -(*** Example 3.8 ***) - -val ex_thy = - thy - |> Theory.add_consts - [("P", "'a => tr", NoSyn), - ("F", "'a => 'a", NoSyn), - ("G", "'a => 'a", NoSyn), - ("H", "'a => 'b => 'b", NoSyn), - ("K", "('a => 'b => 'b) => ('a => 'b => 'b)", NoSyn)] - |> add_axioms - [("F_strict", "F(UU) = UU"), - ("K", "K = (%h x y. P(x) => y | F(h(G(x),y)))"), - ("H", "H = FIX(K)")] - |> Theory.add_name "Ex 3.8"; - -val ax = get_axiom ex_thy; - -val F_strict = ax"F_strict"; -val K = ax"K"; -val H = ax"H"; - -val ex_ss = LCF_ss addsimps [F_strict,K]; - -goal ex_thy "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))"; -by (stac H 1); -by (induct_tac "K::('a=>'b=>'b)=>('a=>'b=>'b)" 1); -by (simp_tac ex_ss 1); -by (asm_simp_tac (ex_ss setloop (split_tac [COND_cases_iff])) 1); -result(); - - -(*** Addition with fixpoint of successor ***) - -val ex_thy = - thy - |> Theory.add_consts - [("s", "'a => 'a", NoSyn), - ("p", "'a => 'a => 'a", NoSyn)] - |> add_axioms - [("p_strict", "p(UU) = UU"), - ("p_s", "p(s(x),y) = s(p(x,y))")] - |> Theory.add_name "fix ex"; - -val ax = get_axiom ex_thy; - -val p_strict = ax"p_strict"; -val p_s = ax"p_s"; - -val ex_ss = LCF_ss addsimps [p_strict,p_s]; - -goal ex_thy "p(FIX(s),y) = FIX(s)"; -by (induct_tac "s" 1); -by (simp_tac ex_ss 1); -by (simp_tac ex_ss 1); -result(); - - -(*** Prefixpoints ***) - -val asms = goal thy "[| f(p) << p; !!q. f(q) << q ==> p << q |] ==> FIX(f)=p"; -by (rewtac eq_def); -by (rtac conjI 1); -by (induct_tac "f" 1); -by (rtac minimal 1); -by (strip_tac 1); -by (rtac less_trans 1); -by (resolve_tac asms 2); -by (etac less_ap_term 1); -by (resolve_tac asms 1); -by (rtac (FIX_eq RS eq_imp_less1) 1); -result(); diff -r 5f6b2dd1cd11 -r be73ddff6c5a src/LCF/fix.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/LCF/fix.thy Fri May 08 13:54:45 1998 +0200 @@ -0,0 +1,2 @@ + +fix = LCF diff -r 5f6b2dd1cd11 -r be73ddff6c5a src/LCF/pair.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/LCF/pair.thy Fri May 08 13:54:45 1998 +0200 @@ -0,0 +1,2 @@ + +pair = LCF