Sexp.ML

renamed meson-test.ML to mesontest.ML,
used exact theory names for use_thy

(*  Title: 	HOL/sexp
    ID:         $Id$
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1992  University of Cambridge

For sexp.thy.  S-expressions.
*)

open Sexp;

(** the sexp functional **)

goal Sexp.thy "mono(%Z. range(Leaf) Un range(Numb) Un Z<*>Z)";
by (REPEAT (ares_tac [monoI, subset_refl, Un_mono, uprod_mono] 1));
val Sexp_fun_mono = result();

val Sexp_unfold = Sexp_fun_mono RS (Sexp_def RS def_lfp_Tarski);

(** Induction **)

val major::prems = goal Sexp.thy 
    "[| ii: Sexp;  !!a. P(Leaf(a));   !!k. P(Numb(k));   \
\       !!i j. [| i: Sexp; j: Sexp; P(i); P(j) |] ==> P(i.j) \
\    |]  ==> P(ii)";
by (rtac (major RS (Sexp_def RS def_induct)) 1);
by (rtac Sexp_fun_mono 1);
by (fast_tac (set_cs addIs prems addSEs [uprodE]) 1);
val Sexp_induct = result();

(** Sexp_case **)

goalw Sexp.thy [Sexp_case_def] "Sexp_case(Leaf(a),c,d,e) = c(a)";
by (fast_tac (HOL_cs addIs  [select_equality] 
	             addSDs [Leaf_inject]
		     addSEs [Leaf_neq_Scons, Leaf_neq_Numb]) 1);
val Sexp_case_Leaf = result();

goalw Sexp.thy [Sexp_case_def] "Sexp_case(Numb(k),c,d,e) = d(k)";
by (fast_tac (HOL_cs addIs  [select_equality] 
	             addSDs [Numb_inject]
		     addSEs [Numb_neq_Scons, Numb_neq_Leaf]) 1);
val Sexp_case_Numb = result();

goalw Sexp.thy [Sexp_case_def] "Sexp_case(M.N, c, d, e) = e(M,N)";
by (fast_tac (HOL_cs addIs  [select_equality] 
	             addSDs [Scons_inject]
	             addSEs [Scons_neq_Leaf, Scons_neq_Numb]) 1);
val Sexp_case_Scons = result();


(** Introduction rules for Sexp constructors **)

val SexpI = Sexp_unfold RS equalityD2 RS subsetD;

goal Sexp.thy "Leaf(a): Sexp";
by (fast_tac (set_cs addIs [SexpI]) 1);
val Sexp_LeafI = result();

goal Sexp.thy "Numb(a): Sexp";
by (fast_tac (set_cs addIs [SexpI]) 1);
val Sexp_NumbI = result();

val prems = goal Sexp.thy 
    "[| M: Sexp;  N: Sexp |] ==> M.N : Sexp";
by (fast_tac (set_cs addIs ([uprodI,SexpI]@prems)) 1);
val Sexp_SconsI = result();

val [prem] = goalw Sexp.thy [In0_def] 
    "M: Sexp ==> In0(M) : Sexp";
by (rtac (prem RS (Sexp_NumbI RS Sexp_SconsI)) 1);
val Sexp_In0I = result();

val [prem] = goalw Sexp.thy [In1_def] 
    "M: Sexp ==> In1(M) : Sexp";
by (rtac (prem RS (Sexp_NumbI RS Sexp_SconsI)) 1);
val Sexp_In1I = result();

goal Sexp.thy "range(Leaf) <= Sexp";
by (fast_tac (set_cs addIs [SexpI]) 1);
val range_Leaf_subset_Sexp = result();

val [major] = goal Sexp.thy "M.N : Sexp ==> M: Sexp & N: Sexp";
by (rtac (major RS setup_induction) 1);
by (etac Sexp_induct 1);
by (ALLGOALS 
    (fast_tac (set_cs addSEs [Scons_neq_Leaf,Scons_neq_Numb,Scons_inject])));
val Scons_D = result();

(** Introduction rules for 'pred_Sexp' **)

val sexp_cs = set_cs addIs [SigmaI, uprodI, SexpI];

goalw Sexp.thy [pred_Sexp_def] "pred_Sexp <= Sigma(Sexp, %u.Sexp)";
by (fast_tac sexp_cs 1);
val pred_Sexp_subset_Sigma = result();

(* <a,b> : pred_Sexp^+ ==> a : Sexp *)
val trancl_pred_SexpD1 = 
    pred_Sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD1
and trancl_pred_SexpD2 = 
    pred_Sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2;

val prems = goalw Sexp.thy [pred_Sexp_def]
    "[| M: Sexp;  N: Sexp |] ==> <M, M.N> : pred_Sexp";
by (fast_tac (set_cs addIs prems) 1);
val pred_SexpI1 = result();

val prems = goalw Sexp.thy [pred_Sexp_def]
    "[| M: Sexp;  N: Sexp |] ==> <N, M.N> : pred_Sexp";
by (fast_tac (set_cs addIs prems) 1);
val pred_SexpI2 = result();

(*Combinations involving transitivity and the rules above*)
val pred_Sexp_t1 = pred_SexpI1 RS r_into_trancl
and pred_Sexp_t2 = pred_SexpI2 RS r_into_trancl;

val pred_Sexp_trans1 = pred_Sexp_t1 RSN (2, trans_trancl RS transD)
and pred_Sexp_trans2 = pred_Sexp_t2 RSN (2, trans_trancl RS transD);

(*Proves goals of the form <M,N>:pred_Sexp^+ provided M,N:Sexp*)
val pred_Sexp_simps =
            [Sexp_LeafI, Sexp_NumbI, Sexp_SconsI, 
	     pred_Sexp_t1, pred_Sexp_t2,
	     pred_Sexp_trans1, pred_Sexp_trans2, cut_apply];
val pred_Sexp_ss = HOL_ss addsimps pred_Sexp_simps;

val major::prems = goalw Sexp.thy [pred_Sexp_def]
    "[| p : pred_Sexp;  \
\       !!M N. [| p = <M, M.N>;  M: Sexp;  N: Sexp |] ==> R; \
\       !!M N. [| p = <N, M.N>;  M: Sexp;  N: Sexp |] ==> R  \
\    |] ==> R";
by (cut_facts_tac [major] 1);
by (REPEAT (eresolve_tac ([asm_rl,emptyE,insertE,UN_E]@prems) 1));
val pred_SexpE = result();

goal Sexp.thy "wf(pred_Sexp)";
by (rtac (pred_Sexp_subset_Sigma RS wfI) 1);
by (etac Sexp_induct 1);
by (fast_tac (HOL_cs addSEs [mp, pred_SexpE, Pair_inject, Scons_inject]) 3);
by (fast_tac (HOL_cs addSEs [mp, pred_SexpE, Pair_inject, Numb_neq_Scons]) 2);
by (fast_tac (HOL_cs addSEs [mp, pred_SexpE, Pair_inject, Leaf_neq_Scons]) 1);
val wf_pred_Sexp = result();

(*** Sexp_rec -- by wf recursion on pred_Sexp ***)

(** conversion rules **)

val Sexp_rec_unfold = wf_pred_Sexp RS (Sexp_rec_def RS def_wfrec);


goal Sexp.thy "Sexp_rec(Leaf(a), c, d, h) = c(a)";
by (stac Sexp_rec_unfold 1);
by (rtac Sexp_case_Leaf 1);
val Sexp_rec_Leaf = result();

goal Sexp.thy "Sexp_rec(Numb(k), c, d, h) = d(k)";
by (stac Sexp_rec_unfold 1);
by (rtac Sexp_case_Numb 1);
val Sexp_rec_Numb = result();

goal Sexp.thy "!!M. [| M: Sexp;  N: Sexp |] ==> \
\    Sexp_rec(M.N, c, d, h) = h(M, N, Sexp_rec(M,c,d,h), Sexp_rec(N,c,d,h))";
by (rtac (Sexp_rec_unfold RS trans) 1);
by (asm_simp_tac(HOL_ss addsimps
               [Sexp_case_Scons,pred_SexpI1,pred_SexpI2,cut_apply])1);
val Sexp_rec_Scons = result();