src/HOL/Induct/Sexp.thy
 changeset 13079 e7738aa7267f parent 11481 c77e5401f2ff child 16417 9bc16273c2d4
equal 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"`
`    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`