src/HOL/ex/Recdefs.ML
author oheimb
Mon, 21 Sep 1998 23:03:11 +0200
changeset 5518 654ead0ba4f7
parent 5124 1ce3cccfacdb
child 5655 afd75136b236
permissions -rw-r--r--
re-added mem and list_all
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
Addsimps qsort.rules;
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    11
5518
654ead0ba4f7 re-added mem and list_all
oheimb
parents: 5124
diff changeset
    12
Goal "(x: set (qsort (ord,l))) = (x: set l)";
5124
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    13
by (res_inst_tac [("u","ord"),("v","l")] qsort.induct 1);
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    14
by (ALLGOALS Asm_simp_tac);
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    15
by (Blast_tac 1);
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    16
qed "qsort_mem_stable";
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    17
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    18
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    19
(** The silly g function: example of nested recursion **)
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    20
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    21
Addsimps g.rules;
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    22
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    23
Goal "g x < Suc x";
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    24
by (res_inst_tac [("u","x")] g.induct 1);
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    25
by Auto_tac;
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    26
by (trans_tac 1);
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    27
qed "g_terminates";
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    28
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    29
Goal "g x = 0";
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    30
by (res_inst_tac [("u","x")] g.induct 1);
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    31
by (ALLGOALS (asm_simp_tac (simpset() addsimps [g_terminates])));
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    32
qed "g_zero";
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    33
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    34
(*** the contrived `mapf' ***)
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    35
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    36
(* proving the termination condition: *)
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    37
val [tc] = mapf.tcs;
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    38
goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc));
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    39
by (rtac allI 1);
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    40
by (case_tac "n=0" 1);
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    41
by (ALLGOALS Asm_simp_tac);
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    42
val lemma = result();
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    43
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    44
(* removing the termination condition from the generated thms: *)
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    45
val [mapf_0,mapf_Suc] = mapf.rules;
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    46
val mapf_Suc = lemma RS mapf_Suc;
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    47
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    48
val mapf_induct = lemma RS mapf.induct;