src/HOL/ex/Recdefs.ML
author paulson
Fri, 10 Mar 2000 17:53:16 +0100
changeset 8415 852c63072334
parent 6451 bc943acc5fda
child 8624 69619f870939
permissions -rw-r--r--
tidied
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$
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
     3
    Author:     Konrad Lawrence C Paulson
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
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    12
Addsimps g.rules;
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";
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    15
by (res_inst_tac [("u","x")] g.induct 1);
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";
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    20
by (res_inst_tac [("u","x")] g.induct 1);
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: *)
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    35
val [mapf_0,mapf_Suc] = mapf.rules;
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;