proper thy files;
authorwenzelm
Fri May 08 13:54:45 1998 +0200 (1998-05-08)
changeset 4905be73ddff6c5a
parent 4904 5f6b2dd1cd11
child 4906 0537ee95d004
proper thy files;
src/LCF/IsaMakefile
src/LCF/ROOT.ML
src/LCF/ex/Ex1.ML
src/LCF/ex/Ex1.thy
src/LCF/ex/Ex2.ML
src/LCF/ex/Ex2.thy
src/LCF/ex/Ex3.ML
src/LCF/ex/Ex3.thy
src/LCF/ex/Ex4.ML
src/LCF/ex/Ex4.thy
src/LCF/ex/ROOT.ML
src/LCF/ex/ex.ML
src/LCF/fix.thy
src/LCF/pair.thy
     1.1 --- a/src/LCF/IsaMakefile	Fri May 08 10:15:39 1998 +0200
     1.2 +++ b/src/LCF/IsaMakefile	Fri May 08 13:54:45 1998 +0200
     1.3 @@ -26,7 +26,8 @@
     1.4  FOL:
     1.5  	@cd $(SRC)/FOL; $(ISATOOL) make FOL
     1.6  
     1.7 -$(OUT)/LCF: $(OUT)/FOL LCF.ML LCF.thy ROOT.ML fix.ML pair.ML simpdata.ML
     1.8 +$(OUT)/LCF: $(OUT)/FOL LCF.ML LCF.thy ROOT.ML fix.ML fix.thy pair.ML \
     1.9 +  pair.thy simpdata.ML
    1.10  	@$(ISATOOL) usedir -b $(OUT)/FOL LCF
    1.11  
    1.12  
    1.13 @@ -34,7 +35,8 @@
    1.14  
    1.15  LCF-ex: LCF $(LOG)/LCF-ex.gz
    1.16  
    1.17 -$(LOG)/LCF-ex.gz: $(OUT)/LCF ex/ROOT.ML ex/ex.ML
    1.18 +$(LOG)/LCF-ex.gz: $(OUT)/LCF ex/Ex1.ML ex/Ex1.thy ex/Ex2.ML ex/Ex2.thy \
    1.19 +  ex/Ex3.ML ex/Ex3.thy ex/Ex4.ML ex/Ex4.thy ex/ROOT.ML
    1.20  	@$(ISATOOL) usedir $(OUT)/LCF ex
    1.21  
    1.22  
     2.1 --- a/src/LCF/ROOT.ML	Fri May 08 10:15:39 1998 +0200
     2.2 +++ b/src/LCF/ROOT.ML	Fri May 08 13:54:45 1998 +0200
     2.3 @@ -14,7 +14,7 @@
     2.4  print_depth 1;
     2.5  use_thy "LCF";
     2.6  use"simpdata.ML";
     2.7 -use"pair.ML";
     2.8 -use"fix.ML";
     2.9 +use_thy"pair";
    2.10 +use_thy"fix";
    2.11  
    2.12  val LCF_build_completed = ();   (*indicate successful build*)
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/LCF/ex/Ex1.ML	Fri May 08 13:54:45 1998 +0200
     3.3 @@ -0,0 +1,28 @@
     3.4 +
     3.5 +simpset_ref() := LCF_ss;
     3.6 +
     3.7 +Addsimps [P_strict,K];
     3.8 +
     3.9 +val H_unfold = prove_goal thy "H = K(H)"
    3.10 + (fn _ => [stac H 1, rtac (FIX_eq RS sym) 1]);
    3.11 +
    3.12 +bind_thm ("H_unfold", H_unfold);
    3.13 +
    3.14 +
    3.15 +val H_strict = prove_goal thy "H(UU)=UU"
    3.16 + (fn _ => [stac H_unfold 1, Simp_tac 1]);
    3.17 +
    3.18 +bind_thm ("H_strict", H_strict);
    3.19 +Addsimps [H_strict];
    3.20 +
    3.21 +goal thy "ALL x. H(FIX(K,x)) = FIX(K,x)";
    3.22 +by (induct_tac "K" 1);
    3.23 +by (Simp_tac 1);
    3.24 +by (simp_tac (simpset() setloop (split_tac [COND_cases_iff])) 1);
    3.25 +by (strip_tac 1);
    3.26 +by (stac H_unfold 1);
    3.27 +by (Asm_simp_tac 1);
    3.28 +qed "H_idemp_lemma";
    3.29 +
    3.30 +val H_idemp = rewrite_rule [mk_meta_eq (H RS sym)] H_idemp_lemma;
    3.31 +bind_thm ("H_idemp", H_idemp);
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/LCF/ex/Ex1.thy	Fri May 08 13:54:45 1998 +0200
     4.3 @@ -0,0 +1,17 @@
     4.4 +
     4.5 +(***  Section 10.4  ***)
     4.6 +
     4.7 +Ex1 = LCF +
     4.8 +
     4.9 +consts
    4.10 +  P	:: "'a => tr"
    4.11 +  G	:: "'a => 'a"
    4.12 +  H	:: "'a => 'a"
    4.13 +  K	:: "('a => 'a) => ('a => 'a)"
    4.14 +
    4.15 +rules
    4.16 +  P_strict	"P(UU) = UU"
    4.17 +  K		"K = (%h x. P(x) => x | h(h(G(x))))"
    4.18 +  H		"H = FIX(K)"
    4.19 +
    4.20 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/LCF/ex/Ex2.ML	Fri May 08 13:54:45 1998 +0200
     5.3 @@ -0,0 +1,11 @@
     5.4 +
     5.5 +simpset_ref() := LCF_ss;
     5.6 +
     5.7 +Addsimps [F_strict,K];
     5.8 +
     5.9 +goal thy "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))";
    5.10 +by (stac H 1);
    5.11 +by (induct_tac "K::('a=>'b=>'b)=>('a=>'b=>'b)" 1);
    5.12 +by (Simp_tac 1);
    5.13 +by (asm_simp_tac (simpset() setloop (split_tac [COND_cases_iff])) 1);
    5.14 +qed "example";
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/LCF/ex/Ex2.thy	Fri May 08 13:54:45 1998 +0200
     6.3 @@ -0,0 +1,18 @@
     6.4 +
     6.5 +(***  Example 3.8  ***)
     6.6 +
     6.7 +Ex2 = LCF +
     6.8 +
     6.9 +consts
    6.10 +  P	:: "'a => tr"
    6.11 +  F	:: "'a => 'a"
    6.12 +  G	:: "'a => 'a"
    6.13 +  H	:: "'a => 'b => 'b"
    6.14 +  K	:: "('a => 'b => 'b) => ('a => 'b => 'b)"
    6.15 +
    6.16 +rules
    6.17 +  F_strict	"F(UU) = UU"
    6.18 +  K		"K = (%h x y. P(x) => y | F(h(G(x),y)))"
    6.19 +  H		"H = FIX(K)"
    6.20 +
    6.21 +end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/LCF/ex/Ex3.ML	Fri May 08 13:54:45 1998 +0200
     7.3 @@ -0,0 +1,11 @@
     7.4 +
     7.5 +simpset_ref() := LCF_ss;
     7.6 +
     7.7 +Addsimps [p_strict,p_s];
     7.8 +
     7.9 +goal thy "p(FIX(s),y) = FIX(s)";
    7.10 +by (induct_tac "s" 1);
    7.11 +by (Simp_tac 1);
    7.12 +by (Simp_tac 1);
    7.13 +qed "example";
    7.14 +
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/LCF/ex/Ex3.thy	Fri May 08 13:54:45 1998 +0200
     8.3 @@ -0,0 +1,14 @@
     8.4 +
     8.5 +(*** Addition with fixpoint of successor ***)
     8.6 +
     8.7 +Ex3 = LCF +
     8.8 +
     8.9 +consts
    8.10 +  s	:: "'a => 'a"
    8.11 +  p	:: "'a => 'a => 'a"
    8.12 +
    8.13 +rules
    8.14 +  p_strict	"p(UU) = UU"
    8.15 +  p_s		"p(s(x),y) = s(p(x,y))"
    8.16 +
    8.17 +end
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/LCF/ex/Ex4.ML	Fri May 08 13:54:45 1998 +0200
     9.3 @@ -0,0 +1,13 @@
     9.4 +
     9.5 +val asms = goal thy "[| f(p) << p; !!q. f(q) << q ==> p << q |] ==> FIX(f)=p";
     9.6 +by (rewtac eq_def);
     9.7 +by (rtac conjI 1);
     9.8 +by (induct_tac "f" 1);
     9.9 +by (rtac minimal 1);
    9.10 +by (strip_tac 1);
    9.11 +by (rtac less_trans 1);
    9.12 +by (resolve_tac asms 2);
    9.13 +by (etac less_ap_term 1);
    9.14 +by (resolve_tac asms 1);
    9.15 +by (rtac (FIX_eq RS eq_imp_less1) 1);
    9.16 +qed "example";
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/LCF/ex/Ex4.thy	Fri May 08 13:54:45 1998 +0200
    10.3 @@ -0,0 +1,4 @@
    10.4 +
    10.5 +(*** Prefixpoints ***)
    10.6 +
    10.7 +Ex4 = LCF
    11.1 --- a/src/LCF/ex/ROOT.ML	Fri May 08 10:15:39 1998 +0200
    11.2 +++ b/src/LCF/ex/ROOT.ML	Fri May 08 13:54:45 1998 +0200
    11.3 @@ -1,7 +1,17 @@
    11.4 +(*  Title:      LCF/ex/ROOT.ML
    11.5 +    ID:         $Id$
    11.6 +    Author:     Tobias Nipkow
    11.7 +    Copyright   1991  University of Cambridge
    11.8 +
    11.9 +Some examples from Lawrence Paulson's book Logic and Computation.
   11.10 +*)
   11.11  
   11.12  writeln"Root file for LCF examples";
   11.13  LCF_build_completed;    (*Cause examples to fail if LCF did*)
   11.14  
   11.15  set proof_timing;
   11.16  
   11.17 -use "ex.ML";
   11.18 +use_thy "Ex1";
   11.19 +use_thy "Ex2";
   11.20 +use_thy "Ex3";
   11.21 +use_thy "Ex4";
    12.1 --- a/src/LCF/ex/ex.ML	Fri May 08 10:15:39 1998 +0200
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,128 +0,0 @@
    12.4 -(*  Title:      LCF/ex/ex.ML
    12.5 -    ID:         $Id$
    12.6 -    Author:     Tobias Nipkow
    12.7 -    Copyright   1991  University of Cambridge
    12.8 -
    12.9 -Some examples from Lawrence Paulson's book Logic and Computation.
   12.10 -*)
   12.11 -
   12.12 -
   12.13 -val add_axioms = PureThy.add_axioms o map Attribute.none;
   12.14 -
   12.15 -
   12.16 -(***  Section 10.4  ***)
   12.17 -
   12.18 -val ex_thy =
   12.19 -  thy
   12.20 -  |> Theory.add_consts
   12.21 -   [("P", "'a => tr", NoSyn),
   12.22 -    ("G", "'a => 'a", NoSyn),
   12.23 -    ("H", "'a => 'a", NoSyn),
   12.24 -    ("K", "('a => 'a) => ('a => 'a)", NoSyn)]
   12.25 -  |> add_axioms
   12.26 -   [("P_strict", "P(UU) = UU"),
   12.27 -    ("K", "K = (%h x. P(x) => x | h(h(G(x))))"),
   12.28 -    ("H", "H = FIX(K)")]
   12.29 -  |> Theory.add_name "Ex 10.4";
   12.30 -
   12.31 -val ax = get_axiom ex_thy;
   12.32 -
   12.33 -val P_strict = ax"P_strict";
   12.34 -val K = ax"K";
   12.35 -val H = ax"H";
   12.36 -
   12.37 -val ex_ss = LCF_ss addsimps [P_strict,K];
   12.38 -
   12.39 -
   12.40 -val H_unfold = prove_goal ex_thy "H = K(H)"
   12.41 - (fn _ => [stac H 1, rtac (FIX_eq RS sym) 1]);
   12.42 -
   12.43 -val H_strict = prove_goal ex_thy "H(UU)=UU"
   12.44 - (fn _ => [stac H_unfold 1, simp_tac ex_ss 1]);
   12.45 -
   12.46 -val ex_ss = ex_ss addsimps [H_strict];
   12.47 -
   12.48 -goal ex_thy "ALL x. H(FIX(K,x)) = FIX(K,x)";
   12.49 -by (induct_tac "K" 1);
   12.50 -by (simp_tac ex_ss 1);
   12.51 -by (simp_tac (ex_ss setloop (split_tac [COND_cases_iff])) 1);
   12.52 -by (strip_tac 1);
   12.53 -by (stac H_unfold 1);
   12.54 -by (asm_simp_tac ex_ss 1);
   12.55 -val H_idemp_lemma = topthm();
   12.56 -
   12.57 -val H_idemp = rewrite_rule [mk_meta_eq (H RS sym)] H_idemp_lemma;
   12.58 -
   12.59 -
   12.60 -(***  Example 3.8  ***)
   12.61 -
   12.62 -val ex_thy =
   12.63 -  thy
   12.64 -  |> Theory.add_consts
   12.65 -   [("P", "'a => tr", NoSyn),
   12.66 -    ("F", "'a => 'a", NoSyn),
   12.67 -    ("G", "'a => 'a", NoSyn),
   12.68 -    ("H", "'a => 'b => 'b", NoSyn),
   12.69 -    ("K", "('a => 'b => 'b) => ('a => 'b => 'b)", NoSyn)]
   12.70 -  |> add_axioms
   12.71 -   [("F_strict", "F(UU) = UU"),
   12.72 -    ("K", "K = (%h x y. P(x) => y | F(h(G(x),y)))"),
   12.73 -    ("H", "H = FIX(K)")]
   12.74 -  |> Theory.add_name "Ex 3.8";
   12.75 -
   12.76 -val ax = get_axiom ex_thy;
   12.77 -
   12.78 -val F_strict = ax"F_strict";
   12.79 -val K = ax"K";
   12.80 -val H = ax"H";
   12.81 -
   12.82 -val ex_ss = LCF_ss addsimps [F_strict,K];
   12.83 -
   12.84 -goal ex_thy "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))";
   12.85 -by (stac H 1);
   12.86 -by (induct_tac "K::('a=>'b=>'b)=>('a=>'b=>'b)" 1);
   12.87 -by (simp_tac ex_ss 1);
   12.88 -by (asm_simp_tac (ex_ss setloop (split_tac [COND_cases_iff])) 1);
   12.89 -result();
   12.90 -
   12.91 -
   12.92 -(*** Addition with fixpoint of successor ***)
   12.93 -
   12.94 -val ex_thy =
   12.95 -  thy
   12.96 -  |> Theory.add_consts
   12.97 -   [("s", "'a => 'a", NoSyn),
   12.98 -    ("p", "'a => 'a => 'a", NoSyn)]
   12.99 -  |> add_axioms
  12.100 -   [("p_strict", "p(UU) = UU"),
  12.101 -    ("p_s", "p(s(x),y) = s(p(x,y))")]
  12.102 -  |> Theory.add_name "fix ex";
  12.103 -
  12.104 -val ax = get_axiom ex_thy;
  12.105 -
  12.106 -val p_strict = ax"p_strict";
  12.107 -val p_s = ax"p_s";
  12.108 -
  12.109 -val ex_ss = LCF_ss addsimps [p_strict,p_s];
  12.110 -
  12.111 -goal ex_thy "p(FIX(s),y) = FIX(s)";
  12.112 -by (induct_tac "s" 1);
  12.113 -by (simp_tac ex_ss 1);
  12.114 -by (simp_tac ex_ss 1);
  12.115 -result();
  12.116 -
  12.117 -
  12.118 -(*** Prefixpoints ***)
  12.119 -
  12.120 -val asms = goal thy "[| f(p) << p; !!q. f(q) << q ==> p << q |] ==> FIX(f)=p";
  12.121 -by (rewtac eq_def);
  12.122 -by (rtac conjI 1);
  12.123 -by (induct_tac "f" 1);
  12.124 -by (rtac minimal 1);
  12.125 -by (strip_tac 1);
  12.126 -by (rtac less_trans 1);
  12.127 -by (resolve_tac asms 2);
  12.128 -by (etac less_ap_term 1);
  12.129 -by (resolve_tac asms 1);
  12.130 -by (rtac (FIX_eq RS eq_imp_less1) 1);
  12.131 -result();
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/LCF/fix.thy	Fri May 08 13:54:45 1998 +0200
    13.3 @@ -0,0 +1,2 @@
    13.4 +
    13.5 +fix = LCF
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/LCF/pair.thy	Fri May 08 13:54:45 1998 +0200
    14.3 @@ -0,0 +1,2 @@
    14.4 +
    14.5 +pair = LCF