# Theory Sexp

Up to index of Isabelle/HOL/Induct

theory Sexp
imports Datatype_Universe Inductive
begin

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