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
     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_case_def] "sexp_case c d e (Leaf a) = c(a)";
    14 by (Blast_tac 1);
    15 qed "sexp_case_Leaf";
    16 
    17 Goalw [sexp_case_def] "sexp_case c d e (Numb k) = d(k)";
    18 by (Blast_tac 1);
    19 qed "sexp_case_Numb";
    20 
    21 Goalw [sexp_case_def] "sexp_case c d e (Scons M N) = e M N";
    22 by (Blast_tac 1);
    23 qed "sexp_case_Scons";
    24 
    25 Addsimps [sexp_case_Leaf, sexp_case_Numb, sexp_case_Scons];
    26 
    27 
    28 (** Introduction rules for sexp constructors **)
    29 
    30 val [prem] = goalw Sexp.thy [In0_def] "M: sexp ==> In0(M) : sexp";
    31 by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
    32 qed "sexp_In0I";
    33 
    34 val [prem] = goalw Sexp.thy [In1_def] "M: sexp ==> In1(M) : sexp";
    35 by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
    36 qed "sexp_In1I";
    37 
    38 AddIs sexp.intrs;
    39 
    40 Goal "range(Leaf) <= sexp";
    41 by (Blast_tac 1);
    42 qed "range_Leaf_subset_sexp";
    43 
    44 val [major] = goal Sexp.thy "Scons M N : sexp ==> M: sexp & N: sexp";
    45 by (rtac (major RS setup_induction) 1);
    46 by (etac sexp.induct 1);
    47 by (ALLGOALS Blast_tac);
    48 qed "Scons_D";
    49 
    50 (** Introduction rules for 'pred_sexp' **)
    51 
    52 Goalw [pred_sexp_def] "pred_sexp <= sexp Times sexp";
    53 by (Blast_tac 1);
    54 qed "pred_sexp_subset_Sigma";
    55 
    56 (* (a,b) : pred_sexp^+ ==> a : sexp *)
    57 val trancl_pred_sexpD1 = 
    58     pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD1
    59 and trancl_pred_sexpD2 = 
    60     pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2;
    61 
    62 Goalw [pred_sexp_def]
    63     "!!M. [| M: sexp;  N: sexp |] ==> (M, Scons M N) : pred_sexp";
    64 by (Blast_tac 1);
    65 qed "pred_sexpI1";
    66 
    67 Goalw [pred_sexp_def]
    68     "!!M. [| M: sexp;  N: sexp |] ==> (N, Scons M N) : pred_sexp";
    69 by (Blast_tac 1);
    70 qed "pred_sexpI2";
    71 
    72 (*Combinations involving transitivity and the rules above*)
    73 val pred_sexp_t1 = pred_sexpI1 RS r_into_trancl
    74 and pred_sexp_t2 = pred_sexpI2 RS r_into_trancl;
    75 
    76 val pred_sexp_trans1 = pred_sexp_t1 RSN (2, trans_trancl RS transD)
    77 and pred_sexp_trans2 = pred_sexp_t2 RSN (2, trans_trancl RS transD);
    78 
    79 (*Proves goals of the form (M,N):pred_sexp^+ provided M,N:sexp*)
    80 Addsimps (sexp.intrs @ [pred_sexp_t1, pred_sexp_t2,
    81                         pred_sexp_trans1, pred_sexp_trans2, cut_apply]);
    82 
    83 val major::prems = goalw Sexp.thy [pred_sexp_def]
    84     "[| p : pred_sexp;                                       \
    85 \       !!M N. [| p = (M, Scons M N);  M: sexp;  N: sexp |] ==> R; \
    86 \       !!M N. [| p = (N, Scons M N);  M: sexp;  N: sexp |] ==> R  \
    87 \    |] ==> R";
    88 by (cut_facts_tac [major] 1);
    89 by (REPEAT (eresolve_tac ([asm_rl,emptyE,insertE,UN_E]@prems) 1));
    90 qed "pred_sexpE";
    91 
    92 Goal "wf(pred_sexp)";
    93 by (rtac (pred_sexp_subset_Sigma RS wfI) 1);
    94 by (etac sexp.induct 1);
    95 by (ALLGOALS (blast_tac (claset() addSEs [allE, pred_sexpE])));
    96 qed "wf_pred_sexp";
    97 
    98 
    99 (*** sexp_rec -- by wf recursion on pred_sexp ***)
   100 
   101 Goal "(%M. sexp_rec M c d e) = wfrec pred_sexp \
   102                        \ (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)))";
   103 by (simp_tac (HOL_ss addsimps [sexp_rec_def]) 1);
   104 
   105 (* sexp_rec a c d e =
   106    sexp_case c d
   107     (%N1 N2.
   108         e N1 N2 (cut (%M. sexp_rec M c d e) pred_sexp a N1)
   109          (cut (%M. sexp_rec M c d e) pred_sexp a N2)) a
   110 *)
   111 bind_thm("sexp_rec_unfold", 
   112 	 [result() RS eq_reflection, wf_pred_sexp] MRS def_wfrec);
   113 
   114 (** conversion rules **)
   115 
   116 Goal "sexp_rec (Leaf a) c d h = c(a)";
   117 by (stac sexp_rec_unfold 1);
   118 by (rtac sexp_case_Leaf 1);
   119 qed "sexp_rec_Leaf";
   120 
   121 Goal "sexp_rec (Numb k) c d h = d(k)";
   122 by (stac sexp_rec_unfold 1);
   123 by (rtac sexp_case_Numb 1);
   124 qed "sexp_rec_Numb";
   125 
   126 Goal "[| M: sexp;  N: sexp |] ==> \
   127 \    sexp_rec (Scons M N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)";
   128 by (rtac (sexp_rec_unfold RS trans) 1);
   129 by (asm_simp_tac (simpset() addsimps [pred_sexpI1, pred_sexpI2]) 1);
   130 qed "sexp_rec_Scons";