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