src/HOL/Induct/Sexp.thy
author blanchet
Thu Jan 16 16:20:17 2014 +0100 (2014-01-16)
changeset 55017 2df6ad1dbd66
parent 44918 6a80fbc4e72c
child 58112 8081087096ad
permissions -rw-r--r--
adapted to move of Wfrec
     1 (*  Title:      HOL/Induct/Sexp.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1992  University of Cambridge
     4 
     5 S-expressions, general binary trees for defining recursive data
     6 structures by hand.
     7 *)
     8 
     9 theory Sexp
    10 imports Main
    11 begin
    12 
    13 type_synonym 'a item = "'a Datatype.item"
    14 abbreviation "Leaf == Datatype.Leaf"
    15 abbreviation "Numb == Datatype.Numb"
    16 
    17 inductive_set
    18   sexp      :: "'a item set"
    19   where
    20     LeafI:  "Leaf(a) \<in> sexp"
    21   | NumbI:  "Numb(i) \<in> sexp"
    22   | SconsI: "[| M \<in> sexp;  N \<in> sexp |] ==> Scons M N \<in> sexp"
    23 
    24 definition
    25   sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, 
    26                 'a item] => 'b" where
    27   "sexp_case c d e M = (THE z. (EX x.   M=Leaf(x) & z=c(x))  
    28                              | (EX k.   M=Numb(k) & z=d(k))  
    29                              | (EX N1 N2. M = Scons N1 N2  & z=e N1 N2))"
    30 
    31 definition
    32   pred_sexp :: "('a item * 'a item)set" where
    33      "pred_sexp = (\<Union>M \<in> sexp. \<Union>N \<in> sexp. {(M, Scons M N), (N, Scons M N)})"
    34 
    35 definition
    36   sexp_rec  :: "['a item, 'a=>'b, nat=>'b,      
    37                 ['a item, 'a item, 'b, 'b]=>'b] => 'b" where
    38    "sexp_rec M c d e = wfrec pred_sexp
    39              (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2))) M"
    40 
    41 
    42 (** sexp_case **)
    43 
    44 lemma sexp_case_Leaf [simp]: "sexp_case c d e (Leaf a) = c(a)"
    45 by (simp add: sexp_case_def, blast)
    46 
    47 lemma sexp_case_Numb [simp]: "sexp_case c d e (Numb k) = d(k)"
    48 by (simp add: sexp_case_def, blast)
    49 
    50 lemma sexp_case_Scons [simp]: "sexp_case c d e (Scons M N) = e M N"
    51 by (simp add: sexp_case_def)
    52 
    53 
    54 
    55 (** Introduction rules for sexp constructors **)
    56 
    57 lemma sexp_In0I: "M \<in> sexp ==> In0(M) \<in> sexp"
    58 apply (simp add: In0_def) 
    59 apply (erule sexp.NumbI [THEN sexp.SconsI])
    60 done
    61 
    62 lemma sexp_In1I: "M \<in> sexp ==> In1(M) \<in> sexp"
    63 apply (simp add: In1_def) 
    64 apply (erule sexp.NumbI [THEN sexp.SconsI])
    65 done
    66 
    67 declare sexp.intros [intro,simp]
    68 
    69 lemma range_Leaf_subset_sexp: "range(Leaf) <= sexp"
    70 by blast
    71 
    72 lemma Scons_D: "Scons M N \<in> sexp ==> M \<in> sexp & N \<in> sexp"
    73   by (induct S == "Scons M N" set: sexp) auto
    74 
    75 (** Introduction rules for 'pred_sexp' **)
    76 
    77 lemma pred_sexp_subset_Sigma: "pred_sexp <= sexp <*> sexp"
    78   by (simp add: pred_sexp_def) blast
    79 
    80 (* (a,b) \<in> pred_sexp^+ ==> a \<in> sexp *)
    81 lemmas trancl_pred_sexpD1 = 
    82     pred_sexp_subset_Sigma
    83          [THEN trancl_subset_Sigma, THEN subsetD, THEN SigmaD1]
    84 and trancl_pred_sexpD2 = 
    85     pred_sexp_subset_Sigma
    86          [THEN trancl_subset_Sigma, THEN subsetD, THEN SigmaD2]
    87 
    88 lemma pred_sexpI1: 
    89     "[| M \<in> sexp;  N \<in> sexp |] ==> (M, Scons M N) \<in> pred_sexp"
    90 by (simp add: pred_sexp_def, blast)
    91 
    92 lemma pred_sexpI2: 
    93     "[| M \<in> sexp;  N \<in> sexp |] ==> (N, Scons M N) \<in> pred_sexp"
    94 by (simp add: pred_sexp_def, blast)
    95 
    96 (*Combinations involving transitivity and the rules above*)
    97 lemmas pred_sexp_t1 [simp] = pred_sexpI1 [THEN r_into_trancl]
    98 and    pred_sexp_t2 [simp] = pred_sexpI2 [THEN r_into_trancl]
    99 
   100 lemmas pred_sexp_trans1 [simp] = trans_trancl [THEN transD, OF _ pred_sexp_t1]
   101 and    pred_sexp_trans2 [simp] = trans_trancl [THEN transD, OF _ pred_sexp_t2]
   102 
   103 (*Proves goals of the form (M,N):pred_sexp^+ provided M,N:sexp*)
   104 declare cut_apply [simp] 
   105 
   106 lemma pred_sexpE:
   107     "[| p \<in> pred_sexp;                                        
   108         !!M N. [| p = (M, Scons M N);  M \<in> sexp;  N \<in> sexp |] ==> R;  
   109         !!M N. [| p = (N, Scons M N);  M \<in> sexp;  N \<in> sexp |] ==> R   
   110      |] ==> R"
   111 by (simp add: pred_sexp_def, blast) 
   112 
   113 lemma wf_pred_sexp: "wf(pred_sexp)"
   114 apply (rule pred_sexp_subset_Sigma [THEN wfI])
   115 apply (erule sexp.induct)
   116 apply (blast elim!: pred_sexpE)+
   117 done
   118 
   119 
   120 (*** sexp_rec -- by wf recursion on pred_sexp ***)
   121 
   122 lemma sexp_rec_unfold_lemma:
   123      "(%M. sexp_rec M c d e) ==
   124       wfrec pred_sexp (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)))"
   125 by (simp add: sexp_rec_def)
   126 
   127 lemmas sexp_rec_unfold = def_wfrec [OF sexp_rec_unfold_lemma wf_pred_sexp]
   128 
   129 (* sexp_rec a c d e =
   130    sexp_case c d
   131     (%N1 N2.
   132         e N1 N2 (cut (%M. sexp_rec M c d e) pred_sexp a N1)
   133          (cut (%M. sexp_rec M c d e) pred_sexp a N2)) a
   134 *)
   135 
   136 (** conversion rules **)
   137 
   138 lemma sexp_rec_Leaf: "sexp_rec (Leaf a) c d h = c(a)"
   139 apply (subst sexp_rec_unfold)
   140 apply (rule sexp_case_Leaf)
   141 done
   142 
   143 lemma sexp_rec_Numb: "sexp_rec (Numb k) c d h = d(k)"
   144 apply (subst sexp_rec_unfold)
   145 apply (rule sexp_case_Numb)
   146 done
   147 
   148 lemma sexp_rec_Scons: "[| M \<in> sexp;  N \<in> sexp |] ==>  
   149      sexp_rec (Scons M N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)"
   150 apply (rule sexp_rec_unfold [THEN trans])
   151 apply (simp add: pred_sexpI1 pred_sexpI2)
   152 done
   153 
   154 end