src/HOL/Sexp.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 5440 f099dffd0f18
child 8703 816d8f6513be
permissions -rw-r--r--
tidying
clasohm@1465
     1
(*  Title:      HOL/Sexp
clasohm@923
     2
    ID:         $Id$
clasohm@1465
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@923
     4
    Copyright   1994  University of Cambridge
clasohm@923
     5
clasohm@923
     6
S-expressions, general binary trees for defining recursive data structures
clasohm@923
     7
*)
clasohm@923
     8
clasohm@923
     9
open Sexp;
clasohm@923
    10
clasohm@923
    11
(** sexp_case **)
clasohm@923
    12
wenzelm@5069
    13
Goalw [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
oheimb@4535
    14
by (Blast_tac 1);
clasohm@923
    15
qed "sexp_case_Leaf";
clasohm@923
    16
wenzelm@5069
    17
Goalw [sexp_case_def] "sexp_case c d e (Numb k) = d(k)";
oheimb@4535
    18
by (Blast_tac 1);
clasohm@923
    19
qed "sexp_case_Numb";
clasohm@923
    20
berghofe@5191
    21
Goalw [sexp_case_def] "sexp_case c d e (Scons M N) = e M N";
oheimb@4535
    22
by (Blast_tac 1);
clasohm@923
    23
qed "sexp_case_Scons";
clasohm@923
    24
paulson@4521
    25
Addsimps [sexp_case_Leaf, sexp_case_Numb, sexp_case_Scons];
paulson@4521
    26
clasohm@923
    27
clasohm@923
    28
(** Introduction rules for sexp constructors **)
clasohm@923
    29
paulson@3029
    30
val [prem] = goalw Sexp.thy [In0_def] "M: sexp ==> In0(M) : sexp";
clasohm@923
    31
by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
clasohm@923
    32
qed "sexp_In0I";
clasohm@923
    33
paulson@3029
    34
val [prem] = goalw Sexp.thy [In1_def] "M: sexp ==> In1(M) : sexp";
clasohm@923
    35
by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
clasohm@923
    36
qed "sexp_In1I";
clasohm@923
    37
oheimb@5440
    38
AddIs sexp.intrs;
berghofe@1760
    39
wenzelm@5069
    40
Goal "range(Leaf) <= sexp";
paulson@2892
    41
by (Blast_tac 1);
clasohm@923
    42
qed "range_Leaf_subset_sexp";
clasohm@923
    43
berghofe@5191
    44
val [major] = goal Sexp.thy "Scons M N : sexp ==> M: sexp & N: sexp";
clasohm@923
    45
by (rtac (major RS setup_induction) 1);
clasohm@923
    46
by (etac sexp.induct 1);
paulson@2892
    47
by (ALLGOALS Blast_tac);
clasohm@923
    48
qed "Scons_D";
clasohm@923
    49
clasohm@923
    50
(** Introduction rules for 'pred_sexp' **)
clasohm@923
    51
wenzelm@5069
    52
Goalw [pred_sexp_def] "pred_sexp <= sexp Times sexp";
paulson@2892
    53
by (Blast_tac 1);
clasohm@923
    54
qed "pred_sexp_subset_Sigma";
clasohm@923
    55
clasohm@972
    56
(* (a,b) : pred_sexp^+ ==> a : sexp *)
clasohm@923
    57
val trancl_pred_sexpD1 = 
clasohm@923
    58
    pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD1
clasohm@923
    59
and trancl_pred_sexpD2 = 
clasohm@923
    60
    pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2;
clasohm@923
    61
wenzelm@5069
    62
Goalw [pred_sexp_def]
berghofe@5191
    63
    "!!M. [| M: sexp;  N: sexp |] ==> (M, Scons M N) : pred_sexp";
paulson@2892
    64
by (Blast_tac 1);
clasohm@923
    65
qed "pred_sexpI1";
clasohm@923
    66
wenzelm@5069
    67
Goalw [pred_sexp_def]
berghofe@5191
    68
    "!!M. [| M: sexp;  N: sexp |] ==> (N, Scons M N) : pred_sexp";
paulson@2892
    69
by (Blast_tac 1);
clasohm@923
    70
qed "pred_sexpI2";
clasohm@923
    71
clasohm@923
    72
(*Combinations involving transitivity and the rules above*)
clasohm@923
    73
val pred_sexp_t1 = pred_sexpI1 RS r_into_trancl
clasohm@923
    74
and pred_sexp_t2 = pred_sexpI2 RS r_into_trancl;
clasohm@923
    75
clasohm@923
    76
val pred_sexp_trans1 = pred_sexp_t1 RSN (2, trans_trancl RS transD)
clasohm@923
    77
and pred_sexp_trans2 = pred_sexp_t2 RSN (2, trans_trancl RS transD);
clasohm@923
    78
clasohm@972
    79
(*Proves goals of the form (M,N):pred_sexp^+ provided M,N:sexp*)
clasohm@1264
    80
Addsimps (sexp.intrs @ [pred_sexp_t1, pred_sexp_t2,
clasohm@1465
    81
                        pred_sexp_trans1, pred_sexp_trans2, cut_apply]);
clasohm@923
    82
clasohm@923
    83
val major::prems = goalw Sexp.thy [pred_sexp_def]
paulson@3029
    84
    "[| p : pred_sexp;                                       \
berghofe@5191
    85
\       !!M N. [| p = (M, Scons M N);  M: sexp;  N: sexp |] ==> R; \
berghofe@5191
    86
\       !!M N. [| p = (N, Scons M N);  M: sexp;  N: sexp |] ==> R  \
clasohm@923
    87
\    |] ==> R";
clasohm@923
    88
by (cut_facts_tac [major] 1);
clasohm@923
    89
by (REPEAT (eresolve_tac ([asm_rl,emptyE,insertE,UN_E]@prems) 1));
clasohm@923
    90
qed "pred_sexpE";
clasohm@923
    91
wenzelm@5069
    92
Goal "wf(pred_sexp)";
clasohm@923
    93
by (rtac (pred_sexp_subset_Sigma RS wfI) 1);
clasohm@923
    94
by (etac sexp.induct 1);
wenzelm@4089
    95
by (ALLGOALS (blast_tac (claset() addSEs [allE, pred_sexpE])));
clasohm@923
    96
qed "wf_pred_sexp";
clasohm@923
    97
paulson@3029
    98
clasohm@923
    99
(*** sexp_rec -- by wf recursion on pred_sexp ***)
clasohm@923
   100
paulson@5278
   101
Goal "(%M. sexp_rec M c d e) = wfrec pred_sexp \
clasohm@1475
   102
                       \ (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)))";
clasohm@1475
   103
by (simp_tac (HOL_ss addsimps [sexp_rec_def]) 1);
paulson@4521
   104
paulson@4521
   105
(* sexp_rec a c d e =
paulson@4521
   106
   sexp_case c d
paulson@4521
   107
    (%N1 N2.
paulson@4521
   108
        e N1 N2 (cut (%M. sexp_rec M c d e) pred_sexp a N1)
paulson@4521
   109
         (cut (%M. sexp_rec M c d e) pred_sexp a N2)) a
paulson@4521
   110
*)
paulson@3029
   111
bind_thm("sexp_rec_unfold", 
paulson@3029
   112
	 [result() RS eq_reflection, wf_pred_sexp] MRS def_wfrec);
clasohm@923
   113
paulson@3029
   114
(** conversion rules **)
clasohm@923
   115
wenzelm@5069
   116
Goal "sexp_rec (Leaf a) c d h = c(a)";
clasohm@923
   117
by (stac sexp_rec_unfold 1);
clasohm@923
   118
by (rtac sexp_case_Leaf 1);
clasohm@923
   119
qed "sexp_rec_Leaf";
clasohm@923
   120
wenzelm@5069
   121
Goal "sexp_rec (Numb k) c d h = d(k)";
clasohm@923
   122
by (stac sexp_rec_unfold 1);
clasohm@923
   123
by (rtac sexp_case_Numb 1);
clasohm@923
   124
qed "sexp_rec_Numb";
clasohm@923
   125
paulson@5143
   126
Goal "[| M: sexp;  N: sexp |] ==> \
berghofe@5191
   127
\    sexp_rec (Scons M N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)";
clasohm@923
   128
by (rtac (sexp_rec_unfold RS trans) 1);
paulson@4521
   129
by (asm_simp_tac (simpset() addsimps [pred_sexpI1, pred_sexpI2]) 1);
clasohm@923
   130
qed "sexp_rec_Scons";