src/HOL/Sexp.ML
author clasohm
Fri, 03 Mar 1995 12:02:25 +0100
changeset 923 ff1574a81019
child 972 e61b058d58d2
permissions -rw-r--r--
new version of HOL with curried function application
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     1
(*  Title: 	HOL/Sexp
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     5
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     6
S-expressions, general binary trees for defining recursive data structures
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     7
*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     8
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     9
open Sexp;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    10
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    11
(** sexp_case **)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    12
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    13
val sexp_free_cs = 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    14
    set_cs addSDs [Leaf_inject, Numb_inject, Scons_inject] 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    15
	   addSEs [Leaf_neq_Scons, Leaf_neq_Numb,
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    16
		   Numb_neq_Scons, Numb_neq_Leaf,
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    17
		   Scons_neq_Leaf, Scons_neq_Numb];
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    18
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    19
goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    20
by (resolve_tac [select_equality] 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    21
by (ALLGOALS (fast_tac sexp_free_cs));
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    22
qed "sexp_case_Leaf";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    23
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    24
goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Numb k) = d(k)";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    25
by (resolve_tac [select_equality] 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    26
by (ALLGOALS (fast_tac sexp_free_cs));
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    27
qed "sexp_case_Numb";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    28
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    29
goalw Sexp.thy [sexp_case_def] "sexp_case c d e (M$N) = e M N";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    30
by (resolve_tac [select_equality] 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    31
by (ALLGOALS (fast_tac sexp_free_cs));
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    32
qed "sexp_case_Scons";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    33
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    34
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    35
(** Introduction rules for sexp constructors **)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    36
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    37
val [prem] = goalw Sexp.thy [In0_def] 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    38
    "M: sexp ==> In0(M) : sexp";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    39
by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    40
qed "sexp_In0I";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    41
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    42
val [prem] = goalw Sexp.thy [In1_def] 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    43
    "M: sexp ==> In1(M) : sexp";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    44
by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    45
qed "sexp_In1I";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    46
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    47
val sexp_cs = set_cs addIs sexp.intrs@[SigmaI, uprodI];
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    48
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    49
goal Sexp.thy "range(Leaf) <= sexp";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    50
by (fast_tac sexp_cs 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    51
qed "range_Leaf_subset_sexp";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    52
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    53
val [major] = goal Sexp.thy "M$N : sexp ==> M: sexp & N: sexp";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    54
by (rtac (major RS setup_induction) 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    55
by (etac sexp.induct 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    56
by (ALLGOALS 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    57
    (fast_tac (set_cs addSEs [Scons_neq_Leaf,Scons_neq_Numb,Scons_inject])));
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    58
qed "Scons_D";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    59
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    60
(** Introduction rules for 'pred_sexp' **)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    61
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    62
goalw Sexp.thy [pred_sexp_def] "pred_sexp <= Sigma sexp (%u.sexp)";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    63
by (fast_tac sexp_cs 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    64
qed "pred_sexp_subset_Sigma";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    65
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    66
(* <a,b> : pred_sexp^+ ==> a : sexp *)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    67
val trancl_pred_sexpD1 = 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    68
    pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD1
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    69
and trancl_pred_sexpD2 = 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    70
    pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    71
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    72
val prems = goalw Sexp.thy [pred_sexp_def]
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    73
    "[| M: sexp;  N: sexp |] ==> <M, M$N> : pred_sexp";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    74
by (fast_tac (set_cs addIs prems) 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    75
qed "pred_sexpI1";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    76
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    77
val prems = goalw Sexp.thy [pred_sexp_def]
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    78
    "[| M: sexp;  N: sexp |] ==> <N, M$N> : pred_sexp";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    79
by (fast_tac (set_cs addIs prems) 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    80
qed "pred_sexpI2";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    81
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    82
(*Combinations involving transitivity and the rules above*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    83
val pred_sexp_t1 = pred_sexpI1 RS r_into_trancl
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    84
and pred_sexp_t2 = pred_sexpI2 RS r_into_trancl;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    85
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    86
val pred_sexp_trans1 = pred_sexp_t1 RSN (2, trans_trancl RS transD)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    87
and pred_sexp_trans2 = pred_sexp_t2 RSN (2, trans_trancl RS transD);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    88
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    89
(*Proves goals of the form <M,N>:pred_sexp^+ provided M,N:sexp*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    90
val pred_sexp_simps =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    91
            sexp.intrs @
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    92
	    [pred_sexp_t1, pred_sexp_t2,
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    93
	     pred_sexp_trans1, pred_sexp_trans2, cut_apply];
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    94
val pred_sexp_ss = HOL_ss addsimps pred_sexp_simps;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    95
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    96
val major::prems = goalw Sexp.thy [pred_sexp_def]
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    97
    "[| p : pred_sexp;  \
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    98
\       !!M N. [| p = <M, M$N>;  M: sexp;  N: sexp |] ==> R; \
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    99
\       !!M N. [| p = <N, M$N>;  M: sexp;  N: sexp |] ==> R  \
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   100
\    |] ==> R";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   101
by (cut_facts_tac [major] 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   102
by (REPEAT (eresolve_tac ([asm_rl,emptyE,insertE,UN_E]@prems) 1));
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   103
qed "pred_sexpE";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   104
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   105
goal Sexp.thy "wf(pred_sexp)";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   106
by (rtac (pred_sexp_subset_Sigma RS wfI) 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   107
by (etac sexp.induct 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   108
by (fast_tac (HOL_cs addSEs [mp, pred_sexpE, Pair_inject, Scons_inject]) 3);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   109
by (fast_tac (HOL_cs addSEs [mp, pred_sexpE, Pair_inject, Numb_neq_Scons]) 2);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   110
by (fast_tac (HOL_cs addSEs [mp, pred_sexpE, Pair_inject, Leaf_neq_Scons]) 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   111
qed "wf_pred_sexp";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   112
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   113
(*** sexp_rec -- by wf recursion on pred_sexp ***)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   114
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   115
(** conversion rules **)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   116
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   117
val sexp_rec_unfold = wf_pred_sexp RS (sexp_rec_def RS def_wfrec);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   118
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   119
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   120
goal Sexp.thy "sexp_rec (Leaf a) c d h = c(a)";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   121
by (stac sexp_rec_unfold 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   122
by (rtac sexp_case_Leaf 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   123
qed "sexp_rec_Leaf";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   124
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   125
goal Sexp.thy "sexp_rec (Numb k) c d h = d(k)";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   126
by (stac sexp_rec_unfold 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   127
by (rtac sexp_case_Numb 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   128
qed "sexp_rec_Numb";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   129
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   130
goal Sexp.thy "!!M. [| M: sexp;  N: sexp |] ==> \
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   131
\    sexp_rec (M$N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   132
by (rtac (sexp_rec_unfold RS trans) 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   133
by (asm_simp_tac(HOL_ss addsimps
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   134
               [sexp_case_Scons,pred_sexpI1,pred_sexpI2,cut_apply])1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   135
qed "sexp_rec_Scons";