src/HOL/Induct/Sexp.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 44918 6a80fbc4e72c
child 55017 2df6ad1dbd66
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8840
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/Induct/Sexp.thy
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
     3
    Copyright   1992  University of Cambridge
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
     4
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
     5
S-expressions, general binary trees for defining recursive data
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
     6
structures by hand.
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
     7
*)
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
     8
44014
88bd7d74a2c1 moved recursion combinator to HOL/Library/Wfrec.thy -- it is so fundamental and well-known that it should survive recdef
krauss
parents: 44013
diff changeset
     9
theory Sexp imports Main "~~/src/HOL/Library/Wfrec" begin
20801
d3616b4abe1b proper import of Main HOL;
wenzelm
parents: 19736
diff changeset
    10
41818
6d4c3ee8219d modernized specifications;
wenzelm
parents: 32960
diff changeset
    11
type_synonym 'a item = "'a Datatype.item"
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20820
diff changeset
    12
abbreviation "Leaf == Datatype.Leaf"
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20820
diff changeset
    13
abbreviation "Numb == Datatype.Numb"
20801
d3616b4abe1b proper import of Main HOL;
wenzelm
parents: 19736
diff changeset
    14
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    15
inductive_set
13079
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    16
  sexp      :: "'a item set"
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    17
  where
13079
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    18
    LeafI:  "Leaf(a) \<in> sexp"
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    19
  | NumbI:  "Numb(i) \<in> sexp"
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    20
  | SconsI: "[| M \<in> sexp;  N \<in> sexp |] ==> Scons M N \<in> sexp"
13079
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    21
19736
wenzelm
parents: 18413
diff changeset
    22
definition
8840
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    23
  sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, 
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20820
diff changeset
    24
                'a item] => 'b" where
20801
d3616b4abe1b proper import of Main HOL;
wenzelm
parents: 19736
diff changeset
    25
  "sexp_case c d e M = (THE z. (EX x.   M=Leaf(x) & z=c(x))  
d3616b4abe1b proper import of Main HOL;
wenzelm
parents: 19736
diff changeset
    26
                             | (EX k.   M=Numb(k) & z=d(k))  
d3616b4abe1b proper import of Main HOL;
wenzelm
parents: 19736
diff changeset
    27
                             | (EX N1 N2. M = Scons N1 N2  & z=e N1 N2))"
8840
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    28
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20820
diff changeset
    29
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20820
diff changeset
    30
  pred_sexp :: "('a item * 'a item)set" where
19736
wenzelm
parents: 18413
diff changeset
    31
     "pred_sexp = (\<Union>M \<in> sexp. \<Union>N \<in> sexp. {(M, Scons M N), (N, Scons M N)})"
8840
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    32
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20820
diff changeset
    33
definition
13079
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    34
  sexp_rec  :: "['a item, 'a=>'b, nat=>'b,      
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20820
diff changeset
    35
                ['a item, 'a item, 'b, 'b]=>'b] => 'b" where
19736
wenzelm
parents: 18413
diff changeset
    36
   "sexp_rec M c d e = wfrec pred_sexp
8840
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
    37
             (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2))) M"
13079
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    38
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    39
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    40
(** sexp_case **)
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    41
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    42
lemma sexp_case_Leaf [simp]: "sexp_case c d e (Leaf a) = c(a)"
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    43
by (simp add: sexp_case_def, blast)
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    44
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    45
lemma sexp_case_Numb [simp]: "sexp_case c d e (Numb k) = d(k)"
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    46
by (simp add: sexp_case_def, blast)
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    47
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    48
lemma sexp_case_Scons [simp]: "sexp_case c d e (Scons M N) = e M N"
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    49
by (simp add: sexp_case_def)
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    50
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    51
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    52
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    53
(** Introduction rules for sexp constructors **)
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    54
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    55
lemma sexp_In0I: "M \<in> sexp ==> In0(M) \<in> sexp"
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    56
apply (simp add: In0_def) 
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    57
apply (erule sexp.NumbI [THEN sexp.SconsI])
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    58
done
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    59
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    60
lemma sexp_In1I: "M \<in> sexp ==> In1(M) \<in> sexp"
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    61
apply (simp add: In1_def) 
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    62
apply (erule sexp.NumbI [THEN sexp.SconsI])
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    63
done
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    64
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    65
declare sexp.intros [intro,simp]
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    66
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    67
lemma range_Leaf_subset_sexp: "range(Leaf) <= sexp"
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    68
by blast
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    69
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    70
lemma Scons_D: "Scons M N \<in> sexp ==> M \<in> sexp & N \<in> sexp"
18413
50c0c118e96d removed obsolete/unused setup_induction;
wenzelm
parents: 16417
diff changeset
    71
  by (induct S == "Scons M N" set: sexp) auto
13079
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    72
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    73
(** Introduction rules for 'pred_sexp' **)
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    74
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    75
lemma pred_sexp_subset_Sigma: "pred_sexp <= sexp <*> sexp"
44918
6a80fbc4e72c tune simpset for Complete_Lattices
noschinl
parents: 44014
diff changeset
    76
  by (simp add: pred_sexp_def) blast
13079
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    77
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    78
(* (a,b) \<in> pred_sexp^+ ==> a \<in> sexp *)
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    79
lemmas trancl_pred_sexpD1 = 
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    80
    pred_sexp_subset_Sigma
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23746
diff changeset
    81
         [THEN trancl_subset_Sigma, THEN subsetD, THEN SigmaD1]
13079
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    82
and trancl_pred_sexpD2 = 
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    83
    pred_sexp_subset_Sigma
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23746
diff changeset
    84
         [THEN trancl_subset_Sigma, THEN subsetD, THEN SigmaD2]
13079
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    85
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    86
lemma pred_sexpI1: 
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    87
    "[| M \<in> sexp;  N \<in> sexp |] ==> (M, Scons M N) \<in> pred_sexp"
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    88
by (simp add: pred_sexp_def, blast)
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    89
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    90
lemma pred_sexpI2: 
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    91
    "[| M \<in> sexp;  N \<in> sexp |] ==> (N, Scons M N) \<in> pred_sexp"
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    92
by (simp add: pred_sexp_def, blast)
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    93
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    94
(*Combinations involving transitivity and the rules above*)
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    95
lemmas pred_sexp_t1 [simp] = pred_sexpI1 [THEN r_into_trancl]
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    96
and    pred_sexp_t2 [simp] = pred_sexpI2 [THEN r_into_trancl]
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    97
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    98
lemmas pred_sexp_trans1 [simp] = trans_trancl [THEN transD, OF _ pred_sexp_t1]
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
    99
and    pred_sexp_trans2 [simp] = trans_trancl [THEN transD, OF _ pred_sexp_t2]
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   100
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   101
(*Proves goals of the form (M,N):pred_sexp^+ provided M,N:sexp*)
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   102
declare cut_apply [simp] 
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   103
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   104
lemma pred_sexpE:
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   105
    "[| p \<in> pred_sexp;                                        
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   106
        !!M N. [| p = (M, Scons M N);  M \<in> sexp;  N \<in> sexp |] ==> R;  
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   107
        !!M N. [| p = (N, Scons M N);  M \<in> sexp;  N \<in> sexp |] ==> R   
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   108
     |] ==> R"
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   109
by (simp add: pred_sexp_def, blast) 
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   110
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   111
lemma wf_pred_sexp: "wf(pred_sexp)"
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   112
apply (rule pred_sexp_subset_Sigma [THEN wfI])
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   113
apply (erule sexp.induct)
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   114
apply (blast elim!: pred_sexpE)+
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   115
done
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   116
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   117
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   118
(*** sexp_rec -- by wf recursion on pred_sexp ***)
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   119
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   120
lemma sexp_rec_unfold_lemma:
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   121
     "(%M. sexp_rec M c d e) ==
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   122
      wfrec pred_sexp (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)))"
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   123
by (simp add: sexp_rec_def)
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   124
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   125
lemmas sexp_rec_unfold = def_wfrec [OF sexp_rec_unfold_lemma wf_pred_sexp]
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   126
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   127
(* sexp_rec a c d e =
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   128
   sexp_case c d
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   129
    (%N1 N2.
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   130
        e N1 N2 (cut (%M. sexp_rec M c d e) pred_sexp a N1)
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   131
         (cut (%M. sexp_rec M c d e) pred_sexp a N2)) a
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   132
*)
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   133
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   134
(** conversion rules **)
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   135
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   136
lemma sexp_rec_Leaf: "sexp_rec (Leaf a) c d h = c(a)"
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   137
apply (subst sexp_rec_unfold)
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   138
apply (rule sexp_case_Leaf)
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   139
done
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   140
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   141
lemma sexp_rec_Numb: "sexp_rec (Numb k) c d h = d(k)"
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   142
apply (subst sexp_rec_unfold)
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   143
apply (rule sexp_case_Numb)
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   144
done
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   145
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   146
lemma sexp_rec_Scons: "[| M \<in> sexp;  N \<in> sexp |] ==>  
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   147
     sexp_rec (Scons M N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)"
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   148
apply (rule sexp_rec_unfold [THEN trans])
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   149
apply (simp add: pred_sexpI1 pred_sexpI2)
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   150
done
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 11481
diff changeset
   151
8840
18b76c137c41 moved theory Sexp to Induct examples;
wenzelm
parents:
diff changeset
   152
end