Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/HOL/Induct/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 4 kB

Quelle Sexp.thy Sprache: Isabelle

(*  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

quality97%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.