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