src/LCF/ex/ex.ML
author paulson
Sat, 10 Jan 1998 17:59:32 +0100
changeset 4552 bb8ff763c93d
parent 4423 a129b817b58a
child 4859 53aa2bc0a22d
permissions -rw-r--r--
Simplified proofs by omitting PA = {|XA, ...|} from RA2
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2820
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      LCF/ex/ex.ML
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
     3
    Author:     Tobias Nipkow
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
     5
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
     6
Some examples from Lawrence Paulson's book Logic and Computation.
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
     7
*)
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
     8
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
     9
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    10
(***  Section 10.4  ***)
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    11
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    12
val ex_thy =
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    13
  thy
3768
67f4ac759100 fully qualified names: Theory.add_XXX;
wenzelm
parents: 2820
diff changeset
    14
  |> Theory.add_consts
2820
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    15
   [("P", "'a => tr", NoSyn),
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    16
    ("G", "'a => 'a", NoSyn),
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    17
    ("H", "'a => 'a", NoSyn),
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    18
    ("K", "('a => 'a) => ('a => 'a)", NoSyn)]
4026
b94dc94be4b7 PureThy.add_store_axioms;
wenzelm
parents: 3768
diff changeset
    19
  |> PureThy.add_store_axioms
2820
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    20
   [("P_strict", "P(UU) = UU"),
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    21
    ("K", "K = (%h x. P(x) => x | h(h(G(x))))"),
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    22
    ("H", "H = FIX(K)")]
3768
67f4ac759100 fully qualified names: Theory.add_XXX;
wenzelm
parents: 2820
diff changeset
    23
  |> Theory.add_name "Ex 10.4";
2820
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    24
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    25
val ax = get_axiom ex_thy;
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    26
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    27
val P_strict = ax"P_strict";
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    28
val K = ax"K";
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    29
val H = ax"H";
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    30
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    31
val ex_ss = LCF_ss addsimps [P_strict,K];
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    32
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    33
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    34
val H_unfold = prove_goal ex_thy "H = K(H)"
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    35
 (fn _ => [stac H 1, rtac (FIX_eq RS sym) 1]);
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    36
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    37
val H_strict = prove_goal ex_thy "H(UU)=UU"
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    38
 (fn _ => [stac H_unfold 1, simp_tac ex_ss 1]);
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    39
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    40
val ex_ss = ex_ss addsimps [H_strict];
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    41
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    42
goal ex_thy "ALL x. H(FIX(K,x)) = FIX(K,x)";
4423
a129b817b58a expandshort;
wenzelm
parents: 4026
diff changeset
    43
by (induct_tac "K" 1);
a129b817b58a expandshort;
wenzelm
parents: 4026
diff changeset
    44
by (simp_tac ex_ss 1);
a129b817b58a expandshort;
wenzelm
parents: 4026
diff changeset
    45
by (simp_tac (ex_ss setloop (split_tac [COND_cases_iff])) 1);
a129b817b58a expandshort;
wenzelm
parents: 4026
diff changeset
    46
by (strip_tac 1);
a129b817b58a expandshort;
wenzelm
parents: 4026
diff changeset
    47
by (stac H_unfold 1);
a129b817b58a expandshort;
wenzelm
parents: 4026
diff changeset
    48
by (asm_simp_tac ex_ss 1);
2820
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    49
val H_idemp_lemma = topthm();
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    50
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    51
val H_idemp = rewrite_rule [mk_meta_eq (H RS sym)] H_idemp_lemma;
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    52
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    53
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    54
(***  Example 3.8  ***)
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    55
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    56
val ex_thy =
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    57
  thy
3768
67f4ac759100 fully qualified names: Theory.add_XXX;
wenzelm
parents: 2820
diff changeset
    58
  |> Theory.add_consts
2820
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    59
   [("P", "'a => tr", NoSyn),
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    60
    ("F", "'a => 'a", NoSyn),
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    61
    ("G", "'a => 'a", NoSyn),
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    62
    ("H", "'a => 'b => 'b", NoSyn),
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    63
    ("K", "('a => 'b => 'b) => ('a => 'b => 'b)", NoSyn)]
4026
b94dc94be4b7 PureThy.add_store_axioms;
wenzelm
parents: 3768
diff changeset
    64
  |> PureThy.add_store_axioms
2820
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    65
   [("F_strict", "F(UU) = UU"),
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    66
    ("K", "K = (%h x y. P(x) => y | F(h(G(x),y)))"),
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    67
    ("H", "H = FIX(K)")]
3768
67f4ac759100 fully qualified names: Theory.add_XXX;
wenzelm
parents: 2820
diff changeset
    68
  |> Theory.add_name "Ex 3.8";
2820
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    69
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    70
val ax = get_axiom ex_thy;
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    71
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    72
val F_strict = ax"F_strict";
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    73
val K = ax"K";
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    74
val H = ax"H";
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    75
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    76
val ex_ss = LCF_ss addsimps [F_strict,K];
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    77
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    78
goal ex_thy "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))";
4423
a129b817b58a expandshort;
wenzelm
parents: 4026
diff changeset
    79
by (stac H 1);
a129b817b58a expandshort;
wenzelm
parents: 4026
diff changeset
    80
by (induct_tac "K::('a=>'b=>'b)=>('a=>'b=>'b)" 1);
a129b817b58a expandshort;
wenzelm
parents: 4026
diff changeset
    81
by (simp_tac ex_ss 1);
a129b817b58a expandshort;
wenzelm
parents: 4026
diff changeset
    82
by (asm_simp_tac (ex_ss setloop (split_tac [COND_cases_iff])) 1);
2820
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    83
result();
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    84
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    85
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    86
(*** Addition with fixpoint of successor ***)
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    87
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    88
val ex_thy =
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    89
  thy
3768
67f4ac759100 fully qualified names: Theory.add_XXX;
wenzelm
parents: 2820
diff changeset
    90
  |> Theory.add_consts
2820
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    91
   [("s", "'a => 'a", NoSyn),
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    92
    ("p", "'a => 'a => 'a", NoSyn)]
4026
b94dc94be4b7 PureThy.add_store_axioms;
wenzelm
parents: 3768
diff changeset
    93
  |> PureThy.add_store_axioms
2820
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    94
   [("p_strict", "p(UU) = UU"),
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    95
    ("p_s", "p(s(x),y) = s(p(x,y))")]
3768
67f4ac759100 fully qualified names: Theory.add_XXX;
wenzelm
parents: 2820
diff changeset
    96
  |> Theory.add_name "fix ex";
2820
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    97
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    98
val ax = get_axiom ex_thy;
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
    99
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
   100
val p_strict = ax"p_strict";
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
   101
val p_s = ax"p_s";
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
   102
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
   103
val ex_ss = LCF_ss addsimps [p_strict,p_s];
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
   104
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
   105
goal ex_thy "p(FIX(s),y) = FIX(s)";
4423
a129b817b58a expandshort;
wenzelm
parents: 4026
diff changeset
   106
by (induct_tac "s" 1);
a129b817b58a expandshort;
wenzelm
parents: 4026
diff changeset
   107
by (simp_tac ex_ss 1);
a129b817b58a expandshort;
wenzelm
parents: 4026
diff changeset
   108
by (simp_tac ex_ss 1);
2820
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
   109
result();
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
   110
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
   111
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
   112
(*** Prefixpoints ***)
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
   113
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
   114
val asms = goal thy "[| f(p) << p; !!q. f(q) << q ==> p << q |] ==> FIX(f)=p";
4423
a129b817b58a expandshort;
wenzelm
parents: 4026
diff changeset
   115
by (rewtac eq_def);
2820
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
   116
by (rtac conjI 1);
4423
a129b817b58a expandshort;
wenzelm
parents: 4026
diff changeset
   117
by (induct_tac "f" 1);
2820
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
   118
by (rtac minimal 1);
4423
a129b817b58a expandshort;
wenzelm
parents: 4026
diff changeset
   119
by (strip_tac 1);
2820
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
   120
by (rtac less_trans 1);
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
   121
by (resolve_tac asms 2);
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
   122
by (etac less_ap_term 1);
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
   123
by (resolve_tac asms 1);
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
   124
by (rtac (FIX_eq RS eq_imp_less1) 1);
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
   125
result();