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