src/HOL/Sexp.ML
author paulson
Thu Sep 12 10:40:05 1996 +0200 (1996-09-12)
changeset 1985 84cf16192e03
parent 1760 6f41a494f3b1
child 2031 03a843f0f447
permissions -rw-r--r--
Tidied many proofs, using AddIffs to let equivalences take
the place of separate Intr and Elim rules. Also deleted most named clasets.
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
clasohm@923
    13
goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
clasohm@1475
    14
by (resolve_tac [select_equality] 1);
berghofe@1760
    15
by (ALLGOALS (Fast_tac));
clasohm@923
    16
qed "sexp_case_Leaf";
clasohm@923
    17
clasohm@923
    18
goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Numb k) = d(k)";
clasohm@1475
    19
by (resolve_tac [select_equality] 1);
berghofe@1760
    20
by (ALLGOALS (Fast_tac));
clasohm@923
    21
qed "sexp_case_Numb";
clasohm@923
    22
clasohm@923
    23
goalw Sexp.thy [sexp_case_def] "sexp_case c d e (M$N) = e M N";
clasohm@1475
    24
by (resolve_tac [select_equality] 1);
berghofe@1760
    25
by (ALLGOALS (Fast_tac));
clasohm@923
    26
qed "sexp_case_Scons";
clasohm@923
    27
clasohm@923
    28
clasohm@923
    29
(** Introduction rules for sexp constructors **)
clasohm@923
    30
clasohm@923
    31
val [prem] = goalw Sexp.thy [In0_def] 
clasohm@923
    32
    "M: sexp ==> In0(M) : sexp";
clasohm@923
    33
by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
clasohm@923
    34
qed "sexp_In0I";
clasohm@923
    35
clasohm@923
    36
val [prem] = goalw Sexp.thy [In1_def] 
clasohm@923
    37
    "M: sexp ==> In1(M) : sexp";
clasohm@923
    38
by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
clasohm@923
    39
qed "sexp_In1I";
clasohm@923
    40
clasohm@923
    41
val sexp_cs = set_cs addIs sexp.intrs@[SigmaI, uprodI];
clasohm@923
    42
berghofe@1760
    43
AddIs (sexp.intrs@[SigmaI, uprodI]);
berghofe@1760
    44
clasohm@923
    45
goal Sexp.thy "range(Leaf) <= sexp";
berghofe@1760
    46
by (Fast_tac 1);
clasohm@923
    47
qed "range_Leaf_subset_sexp";
clasohm@923
    48
clasohm@923
    49
val [major] = goal Sexp.thy "M$N : sexp ==> M: sexp & N: sexp";
clasohm@923
    50
by (rtac (major RS setup_induction) 1);
clasohm@923
    51
by (etac sexp.induct 1);
paulson@1985
    52
by (ALLGOALS Fast_tac);
clasohm@923
    53
qed "Scons_D";
clasohm@923
    54
clasohm@923
    55
(** Introduction rules for 'pred_sexp' **)
clasohm@923
    56
paulson@1642
    57
goalw Sexp.thy [pred_sexp_def] "pred_sexp <= sexp Times sexp";
berghofe@1760
    58
by (Fast_tac 1);
clasohm@923
    59
qed "pred_sexp_subset_Sigma";
clasohm@923
    60
clasohm@972
    61
(* (a,b) : pred_sexp^+ ==> a : sexp *)
clasohm@923
    62
val trancl_pred_sexpD1 = 
clasohm@923
    63
    pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD1
clasohm@923
    64
and trancl_pred_sexpD2 = 
clasohm@923
    65
    pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2;
clasohm@923
    66
clasohm@923
    67
val prems = goalw Sexp.thy [pred_sexp_def]
clasohm@972
    68
    "[| M: sexp;  N: sexp |] ==> (M, M$N) : pred_sexp";
berghofe@1760
    69
by (fast_tac (!claset addIs prems) 1);
clasohm@923
    70
qed "pred_sexpI1";
clasohm@923
    71
clasohm@923
    72
val prems = goalw Sexp.thy [pred_sexp_def]
clasohm@972
    73
    "[| M: sexp;  N: sexp |] ==> (N, M$N) : pred_sexp";
berghofe@1760
    74
by (fast_tac (!claset addIs prems) 1);
clasohm@923
    75
qed "pred_sexpI2";
clasohm@923
    76
clasohm@923
    77
(*Combinations involving transitivity and the rules above*)
clasohm@923
    78
val pred_sexp_t1 = pred_sexpI1 RS r_into_trancl
clasohm@923
    79
and pred_sexp_t2 = pred_sexpI2 RS r_into_trancl;
clasohm@923
    80
clasohm@923
    81
val pred_sexp_trans1 = pred_sexp_t1 RSN (2, trans_trancl RS transD)
clasohm@923
    82
and pred_sexp_trans2 = pred_sexp_t2 RSN (2, trans_trancl RS transD);
clasohm@923
    83
clasohm@972
    84
(*Proves goals of the form (M,N):pred_sexp^+ provided M,N:sexp*)
clasohm@1264
    85
Addsimps (sexp.intrs @ [pred_sexp_t1, pred_sexp_t2,
clasohm@1465
    86
                        pred_sexp_trans1, pred_sexp_trans2, cut_apply]);
clasohm@923
    87
clasohm@923
    88
val major::prems = goalw Sexp.thy [pred_sexp_def]
clasohm@923
    89
    "[| p : pred_sexp;  \
clasohm@972
    90
\       !!M N. [| p = (M, M$N);  M: sexp;  N: sexp |] ==> R; \
clasohm@972
    91
\       !!M N. [| p = (N, M$N);  M: sexp;  N: sexp |] ==> R  \
clasohm@923
    92
\    |] ==> R";
clasohm@923
    93
by (cut_facts_tac [major] 1);
clasohm@923
    94
by (REPEAT (eresolve_tac ([asm_rl,emptyE,insertE,UN_E]@prems) 1));
clasohm@923
    95
qed "pred_sexpE";
clasohm@923
    96
clasohm@923
    97
goal Sexp.thy "wf(pred_sexp)";
clasohm@923
    98
by (rtac (pred_sexp_subset_Sigma RS wfI) 1);
clasohm@923
    99
by (etac sexp.induct 1);
paulson@1985
   100
by (ALLGOALS (fast_tac (!claset addSEs [mp, pred_sexpE])));
clasohm@923
   101
qed "wf_pred_sexp";
clasohm@923
   102
clasohm@923
   103
(*** sexp_rec -- by wf recursion on pred_sexp ***)
clasohm@923
   104
clasohm@1475
   105
goal Sexp.thy
clasohm@1475
   106
   "(%M. sexp_rec M c d e) = wfrec pred_sexp \
clasohm@1475
   107
                       \ (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)))";
clasohm@1475
   108
by (simp_tac (HOL_ss addsimps [sexp_rec_def]) 1);
clasohm@1475
   109
bind_thm("sexp_rec_unfold", wf_pred_sexp RS 
clasohm@1475
   110
                            ((result() RS eq_reflection) RS def_wfrec));
clasohm@923
   111
(** conversion rules **)
clasohm@923
   112
clasohm@1475
   113
(*---------------------------------------------------------------------------
clasohm@1475
   114
 * Old:
clasohm@1475
   115
 * val sexp_rec_unfold = wf_pred_sexp RS (sexp_rec_def RS def_wfrec);
clasohm@1475
   116
 *---------------------------------------------------------------------------*)
clasohm@923
   117
clasohm@923
   118
clasohm@923
   119
goal Sexp.thy "sexp_rec (Leaf a) c d h = c(a)";
clasohm@923
   120
by (stac sexp_rec_unfold 1);
clasohm@923
   121
by (rtac sexp_case_Leaf 1);
clasohm@923
   122
qed "sexp_rec_Leaf";
clasohm@923
   123
clasohm@923
   124
goal Sexp.thy "sexp_rec (Numb k) c d h = d(k)";
clasohm@923
   125
by (stac sexp_rec_unfold 1);
clasohm@923
   126
by (rtac sexp_case_Numb 1);
clasohm@923
   127
qed "sexp_rec_Numb";
clasohm@923
   128
clasohm@923
   129
goal Sexp.thy "!!M. [| M: sexp;  N: sexp |] ==> \
clasohm@923
   130
\    sexp_rec (M$N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)";
clasohm@923
   131
by (rtac (sexp_rec_unfold RS trans) 1);
clasohm@1264
   132
by (asm_simp_tac (!simpset addsimps [sexp_case_Scons,pred_sexpI1,pred_sexpI2])
clasohm@1264
   133
    1);
clasohm@923
   134
qed "sexp_rec_Scons";