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