src/LCF/ex/Ex1.ML
author oheimb
Fri Jun 02 20:38:28 2000 +0200 (2000-06-02)
changeset 9028 8a1ec8f05f14
parent 5061 f947332d5465
child 17248 81bf91654e73
permissions -rw-r--r--
added HOL/Prolog
     1 
     2 simpset_ref() := LCF_ss;
     3 
     4 Addsimps [P_strict,K];
     5 
     6 val H_unfold = prove_goal thy "H = K(H)"
     7  (fn _ => [stac H 1, rtac (FIX_eq RS sym) 1]);
     8 
     9 bind_thm ("H_unfold", H_unfold);
    10 
    11 
    12 val H_strict = prove_goal thy "H(UU)=UU"
    13  (fn _ => [stac H_unfold 1, Simp_tac 1]);
    14 
    15 bind_thm ("H_strict", H_strict);
    16 Addsimps [H_strict];
    17 
    18 Goal "ALL x. H(FIX(K,x)) = FIX(K,x)";
    19 by (induct_tac "K" 1);
    20 by (Simp_tac 1);
    21 by (simp_tac (simpset() setloop (split_tac [COND_cases_iff])) 1);
    22 by (strip_tac 1);
    23 by (stac H_unfold 1);
    24 by (Asm_simp_tac 1);
    25 qed "H_idemp_lemma";
    26 
    27 val H_idemp = rewrite_rule [mk_meta_eq (H RS sym)] H_idemp_lemma;
    28 bind_thm ("H_idemp", H_idemp);