Up to index of Isabelle/HOL/Induct
theory Sexp(* Title: HOL/Induct/Sexp.thy ID: $Id: Sexp.thy,v 1.5 2005/06/17 14:13:07 haftmann Exp $ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge S-expressions, general binary trees for defining recursive data structures by hand. *) theory Sexp imports Datatype_Universe Inductive begin consts sexp :: "'a item set" inductive sexp intros LeafI: "Leaf(a) ∈ sexp" NumbI: "Numb(i) ∈ sexp" SconsI: "[| M ∈ sexp; N ∈ sexp |] ==> Scons M N ∈ sexp" constdefs sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, 'a item] => 'b" "sexp_case c d e M == THE z. (EX x. M=Leaf(x) & z=c(x)) | (EX k. M=Numb(k) & z=d(k)) | (EX N1 N2. M = Scons N1 N2 & z=e N1 N2)" pred_sexp :: "('a item * 'a item)set" "pred_sexp == \<Union>M ∈ sexp. \<Union>N ∈ sexp. {(M, Scons M N), (N, Scons M N)}" sexp_rec :: "['a item, 'a=>'b, nat=>'b, ['a item, 'a item, 'b, 'b]=>'b] => 'b" "sexp_rec M c d e == wfrec pred_sexp (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2))) M" (** sexp_case **) lemma sexp_case_Leaf [simp]: "sexp_case c d e (Leaf a) = c(a)" by (simp add: sexp_case_def, blast) lemma sexp_case_Numb [simp]: "sexp_case c d e (Numb k) = d(k)" by (simp add: sexp_case_def, blast) lemma sexp_case_Scons [simp]: "sexp_case c d e (Scons M N) = e M N" by (simp add: sexp_case_def) (** Introduction rules for sexp constructors **) lemma sexp_In0I: "M ∈ sexp ==> In0(M) ∈ sexp" apply (simp add: In0_def) apply (erule sexp.NumbI [THEN sexp.SconsI]) done lemma sexp_In1I: "M ∈ sexp ==> In1(M) ∈ sexp" apply (simp add: In1_def) apply (erule sexp.NumbI [THEN sexp.SconsI]) done declare sexp.intros [intro,simp] lemma range_Leaf_subset_sexp: "range(Leaf) <= sexp" by blast lemma Scons_D: "Scons M N ∈ sexp ==> M ∈ sexp & N ∈ sexp" apply (erule setup_induction) apply (erule sexp.induct, blast+) done (** Introduction rules for 'pred_sexp' **) lemma pred_sexp_subset_Sigma: "pred_sexp <= sexp <*> sexp" by (simp add: pred_sexp_def, blast) (* (a,b) ∈ pred_sexp^+ ==> a ∈ sexp *) lemmas trancl_pred_sexpD1 = pred_sexp_subset_Sigma [THEN trancl_subset_Sigma, THEN subsetD, THEN SigmaD1] and trancl_pred_sexpD2 = pred_sexp_subset_Sigma [THEN trancl_subset_Sigma, THEN subsetD, THEN SigmaD2] lemma pred_sexpI1: "[| M ∈ sexp; N ∈ sexp |] ==> (M, Scons M N) ∈ pred_sexp" by (simp add: pred_sexp_def, blast) lemma pred_sexpI2: "[| M ∈ sexp; N ∈ sexp |] ==> (N, Scons M N) ∈ pred_sexp" by (simp add: pred_sexp_def, blast) (*Combinations involving transitivity and the rules above*) lemmas pred_sexp_t1 [simp] = pred_sexpI1 [THEN r_into_trancl] and pred_sexp_t2 [simp] = pred_sexpI2 [THEN r_into_trancl] lemmas pred_sexp_trans1 [simp] = trans_trancl [THEN transD, OF _ pred_sexp_t1] and pred_sexp_trans2 [simp] = trans_trancl [THEN transD, OF _ pred_sexp_t2] (*Proves goals of the form (M,N):pred_sexp^+ provided M,N:sexp*) declare cut_apply [simp] lemma pred_sexpE: "[| p ∈ pred_sexp; !!M N. [| p = (M, Scons M N); M ∈ sexp; N ∈ sexp |] ==> R; !!M N. [| p = (N, Scons M N); M ∈ sexp; N ∈ sexp |] ==> R |] ==> R" by (simp add: pred_sexp_def, blast) lemma wf_pred_sexp: "wf(pred_sexp)" apply (rule pred_sexp_subset_Sigma [THEN wfI]) apply (erule sexp.induct) apply (blast elim!: pred_sexpE)+ done (*** sexp_rec -- by wf recursion on pred_sexp ***) lemma sexp_rec_unfold_lemma: "(%M. sexp_rec M c d e) == wfrec pred_sexp (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)))" by (simp add: sexp_rec_def) lemmas sexp_rec_unfold = def_wfrec [OF sexp_rec_unfold_lemma wf_pred_sexp] (* sexp_rec a c d e = sexp_case c d (%N1 N2. e N1 N2 (cut (%M. sexp_rec M c d e) pred_sexp a N1) (cut (%M. sexp_rec M c d e) pred_sexp a N2)) a *) (** conversion rules **) lemma sexp_rec_Leaf: "sexp_rec (Leaf a) c d h = c(a)" apply (subst sexp_rec_unfold) apply (rule sexp_case_Leaf) done lemma sexp_rec_Numb: "sexp_rec (Numb k) c d h = d(k)" apply (subst sexp_rec_unfold) apply (rule sexp_case_Numb) done lemma sexp_rec_Scons: "[| M ∈ sexp; N ∈ sexp |] ==> sexp_rec (Scons M N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)" apply (rule sexp_rec_unfold [THEN trans]) apply (simp add: pred_sexpI1 pred_sexpI2) done end
lemma sexp_case_Leaf:
sexp_case c d e (Leaf a) = c a
lemma sexp_case_Numb:
sexp_case c d e (Numb k) = d k
lemma sexp_case_Scons:
sexp_case c d e (Scons M N) = e M N
lemma sexp_In0I:
M ∈ sexp ==> In0 M ∈ sexp
lemma sexp_In1I:
M ∈ sexp ==> In1 M ∈ sexp
lemma range_Leaf_subset_sexp:
range Leaf ⊆ sexp
lemma Scons_D:
Scons M N ∈ sexp ==> M ∈ sexp ∧ N ∈ sexp
lemma pred_sexp_subset_Sigma:
pred_sexp ⊆ sexp × sexp
lemmas trancl_pred_sexpD1:
(a, b) ∈ pred_sexp+ ==> a ∈ sexp
and trancl_pred_sexpD2:
(a, b) ∈ pred_sexp+ ==> b ∈ sexp
lemmas trancl_pred_sexpD1:
(a, b) ∈ pred_sexp+ ==> a ∈ sexp
and trancl_pred_sexpD2:
(a, b) ∈ pred_sexp+ ==> b ∈ sexp
lemma pred_sexpI1:
[| M ∈ sexp; N ∈ sexp |] ==> (M, Scons M N) ∈ pred_sexp
lemma pred_sexpI2:
[| M ∈ sexp; N ∈ sexp |] ==> (N, Scons M N) ∈ pred_sexp
lemmas pred_sexp_t1:
[| a ∈ sexp; N1 ∈ sexp |] ==> (a, Scons a N1) ∈ pred_sexp+
and pred_sexp_t2:
[| M1 ∈ sexp; a ∈ sexp |] ==> (a, Scons M1 a) ∈ pred_sexp+
lemmas pred_sexp_t1:
[| a ∈ sexp; N1 ∈ sexp |] ==> (a, Scons a N1) ∈ pred_sexp+
and pred_sexp_t2:
[| M1 ∈ sexp; a ∈ sexp |] ==> (a, Scons M1 a) ∈ pred_sexp+
lemmas pred_sexp_trans1:
[| (a, b) ∈ pred_sexp+; b ∈ sexp; N3 ∈ sexp |] ==> (a, Scons b N3) ∈ pred_sexp+
and pred_sexp_trans2:
[| (a, b) ∈ pred_sexp+; M3 ∈ sexp; b ∈ sexp |] ==> (a, Scons M3 b) ∈ pred_sexp+
lemmas pred_sexp_trans1:
[| (a, b) ∈ pred_sexp+; b ∈ sexp; N3 ∈ sexp |] ==> (a, Scons b N3) ∈ pred_sexp+
and pred_sexp_trans2:
[| (a, b) ∈ pred_sexp+; M3 ∈ sexp; b ∈ sexp |] ==> (a, Scons M3 b) ∈ pred_sexp+
lemma pred_sexpE:
[| p ∈ pred_sexp; !!M N. [| p = (M, Scons M N); M ∈ sexp; N ∈ sexp |] ==> R; !!M N. [| p = (N, Scons M N); M ∈ sexp; N ∈ sexp |] ==> R |] ==> R
lemma wf_pred_sexp:
wf pred_sexp
lemma sexp_rec_unfold_lemma:
%M. sexp_rec M c d e == wfrec pred_sexp (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)))
lemmas sexp_rec_unfold:
sexp_rec a c2 d2 e2 = sexp_case c2 d2 (%N1 N2. e2 N1 N2 (cut (%M. sexp_rec M c2 d2 e2) pred_sexp a N1) (cut (%M. sexp_rec M c2 d2 e2) pred_sexp a N2)) a
lemmas sexp_rec_unfold:
sexp_rec a c2 d2 e2 = sexp_case c2 d2 (%N1 N2. e2 N1 N2 (cut (%M. sexp_rec M c2 d2 e2) pred_sexp a N1) (cut (%M. sexp_rec M c2 d2 e2) pred_sexp a N2)) a
lemma sexp_rec_Leaf:
sexp_rec (Leaf a) c d h = c a
lemma sexp_rec_Numb:
sexp_rec (Numb k) c d h = d k
lemma sexp_rec_Scons:
[| M ∈ sexp; N ∈ sexp |] ==> sexp_rec (Scons M N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)