|
(* Title: HOL/Induct/Sexp.thy
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 "HOL-Library.Old_Datatype"
begin
type_synonym 'a item = "'a Old_Datatype.item"
abbreviation "Leaf == Old_Datatype.Leaf"
abbreviation "Numb == Old_Datatype.Numb"
inductive_set
sexp :: "'a item set"
where
LeafI: "Leaf(a) \ sexp"
| NumbI: "Numb(i) \ sexp"
| SconsI: "[| M \ sexp; N \ sexp |] ==> Scons M N \ sexp"
definition
sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b,
'a item] => 'b" where
"sexp_case c d e M = (THE z. (\x. M=Leaf(x) & z=c(x))
| (\<exists>k. M=Numb(k) & z=d(k))
| (\<exists>N1 N2. M = Scons N1 N2 & z=e N1 N2))"
definition
pred_sexp :: "('a item * 'a item)set" where
"pred_sexp = (\M \ sexp. \N \ sexp. {(M, Scons M N), (N, Scons M N)})"
definition
sexp_rec :: "['a item, 'a=>'b, nat=>'b,
['a item, 'a item, 'b, 'b]=>'b] => 'b" where
"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"
by (induct S == "Scons M N" set: sexp) auto
(** Introduction rules for 'pred_sexp' **)
lemma pred_sexp_subset_Sigma: "pred_sexp <= sexp \ sexp"
by (simp add: pred_sexp_def) blast
(* (a,b) \<in> pred_sexp^+ ==> a \<in> 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 \<in> sexp; N \<in> sexp |] ==> R;
!!M N. [| p = (N, Scons M N); M \<in> sexp; N \<in> 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
[ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
]
|
