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--
```     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
```