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