src/HOL/ex/Recdefs.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 9747 043098ba5098
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5124
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/ex/Recdefs.ML
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
8683
9d3e8c4a0287 fixed comment;
wenzelm
parents: 8624
diff changeset
     3
    Author:     Konrad Slind and Lawrence C Paulson
5124
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
     4
    Copyright   1997  University of Cambridge
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
     5
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
     6
A few proofs to demonstrate the functions defined in Recdefs.thy
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
     7
Lemma statements from Konrad Slind's Web site
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
     8
*)
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
     9
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    10
(** The silly g function: example of nested recursion **)
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    11
8624
69619f870939 recdef.rules -> recdef.simps
nipkow
parents: 8415
diff changeset
    12
Addsimps g.simps;
5124
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    13
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    14
Goal "g x < Suc x";
9747
043098ba5098 introduced induct_thm_tac
nipkow
parents: 9736
diff changeset
    15
by (induct_thm_tac g.induct "x" 1);
5124
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    16
by Auto_tac;
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    17
qed "g_terminates";
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    18
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    19
Goal "g x = 0";
9747
043098ba5098 introduced induct_thm_tac
nipkow
parents: 9736
diff changeset
    20
by (induct_thm_tac g.induct "x" 1);
5124
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    21
by (ALLGOALS (asm_simp_tac (simpset() addsimps [g_terminates])));
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    22
qed "g_zero";
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    23
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    24
(*** the contrived `mapf' ***)
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    25
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    26
(* proving the termination condition: *)
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    27
val [tc] = mapf.tcs;
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    28
goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc));
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    29
by (rtac allI 1);
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    30
by (case_tac "n=0" 1);
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    31
by (ALLGOALS Asm_simp_tac);
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    32
val lemma = result();
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    33
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    34
(* removing the termination condition from the generated thms: *)
8624
69619f870939 recdef.rules -> recdef.simps
nipkow
parents: 8415
diff changeset
    35
val [mapf_0,mapf_Suc] = mapf.simps;
5124
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    36
val mapf_Suc = lemma RS mapf_Suc;
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    37
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    38
val mapf_induct = lemma RS mapf.induct;