src/HOL/ex/MT.ML
author clasohm
Wed, 04 Oct 1995 13:12:14 +0100
changeset 1266 3ae9fe3c0f68
parent 1047 5133479a37cf
child 1465 5d7a7e439cec
permissions -rw-r--r--
added local simpsets
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1047
diff changeset
     1
(*  Title: 	HOL/ex/MT.ML
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     3
    Author: 	Jacob Frost, Cambridge University Computer Laboratory
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     5
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     6
Based upon the article
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     7
    Robin Milner and Mads Tofte,
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     8
    Co-induction in Relational Semantics,
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     9
    Theoretical Computer Science 87 (1991), pages 209-220.
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    10
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    11
Written up as
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    12
    Jacob Frost, A Case Study of Co-induction in Isabelle/HOL
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    13
    Report 308, Computer Lab, University of Cambridge (1993).
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
    14
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
    15
NEEDS TO USE INDUCTIVE DEFS PACKAGE
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    16
*)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    17
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    18
open MT;
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    19
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    20
val prems = goal MT.thy "~a:{b} ==> ~a=b";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    21
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    22
by (rtac notI 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    23
by (dtac notE 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    24
by (hyp_subst_tac 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    25
by (rtac singletonI 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    26
by (assume_tac 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    27
qed "notsingletonI";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    28
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    29
(* ############################################################ *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    30
(* Inference systems                                            *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    31
(* ############################################################ *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    32
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    33
val infsys_mono_tac =
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    34
  (rewtac subset_def) THEN (safe_tac HOL_cs) THEN (rtac ballI 1) THEN
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    35
  (rtac CollectI 1) THEN (dtac CollectD 1) THEN
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    36
  REPEAT 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    37
    ( (TRY ((etac disjE 1) THEN (rtac disjI2 2) THEN (rtac disjI1 1))) THEN
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    38
      (REPEAT (etac exE 1)) THEN (REPEAT (rtac exI 1)) THEN (fast_tac set_cs 1)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    39
    );
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    40
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
    41
val prems = goal MT.thy "P a b ==> P (fst (a,b)) (snd (a,b))";
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1047
diff changeset
    42
by (simp_tac (!simpset addsimps prems) 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    43
qed "infsys_p1";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    44
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
    45
val prems = goal MT.thy "!!a b. P (fst (a,b)) (snd (a,b)) ==> P a b";
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1047
diff changeset
    46
by (Asm_full_simp_tac 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    47
qed "infsys_p2";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    48
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    49
val prems = goal MT.thy 
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
    50
 "!!a. P a b c ==> P (fst(fst((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c))";
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1047
diff changeset
    51
by (Asm_full_simp_tac 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    52
qed "infsys_pp1";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    53
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    54
val prems = goal MT.thy 
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
    55
 "!!a. P (fst(fst((a,b),c))) (snd(fst((a,b),c))) (snd((a,b),c)) ==> P a b c";
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1047
diff changeset
    56
by (Asm_full_simp_tac 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    57
qed "infsys_pp2";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    58
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    59
(* ############################################################ *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    60
(* Fixpoints                                                    *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    61
(* ############################################################ *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    62
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    63
(* Least fixpoints *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    64
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    65
val prems = goal MT.thy "[| mono(f); x:f(lfp(f)) |] ==> x:lfp(f)";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    66
by (rtac subsetD 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    67
by (rtac lfp_lemma2 1);
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
    68
by (resolve_tac prems 1);
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
    69
by (resolve_tac prems 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    70
qed "lfp_intro2";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    71
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    72
val prems = goal MT.thy
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    73
  " [| x:lfp(f); mono(f); !!y. y:f(lfp(f)) ==> P(y) |] ==> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    74
\   P(x)";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    75
by (cut_facts_tac prems 1);
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
    76
by (resolve_tac prems 1);
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
    77
by (rtac subsetD 1);
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
    78
by (rtac lfp_lemma3 1);
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
    79
by (assume_tac 1);
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
    80
by (assume_tac 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    81
qed "lfp_elim2";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    82
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    83
val prems = goal MT.thy
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    84
  " [| x:lfp(f); mono(f); !!y. y:f(lfp(f) Int {x.P(x)}) ==> P(y) |] ==> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    85
\   P(x)";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    86
by (cut_facts_tac prems 1);
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
    87
by (etac induct 1);
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
    88
by (assume_tac 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    89
by (eresolve_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    90
qed "lfp_ind2";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    91
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    92
(* Greatest fixpoints *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    93
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    94
(* Note : "[| x:S; S <= f(S Un gfp(f)); mono(f) |] ==> x:gfp(f)" *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    95
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    96
val [cih,monoh] = goal MT.thy "[| x:f({x} Un gfp(f)); mono(f) |] ==> x:gfp(f)";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    97
by (rtac (cih RSN (2,gfp_upperbound RS subsetD)) 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    98
by (rtac (monoh RS monoD) 1);
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
    99
by (rtac (UnE RS subsetI) 1);
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   100
by (assume_tac 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   101
by (fast_tac (set_cs addSIs [cih]) 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   102
by (rtac (monoh RS monoD RS subsetD) 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   103
by (rtac Un_upper2 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   104
by (etac (monoh RS gfp_lemma2 RS subsetD) 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   105
qed "gfp_coind2";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   106
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   107
val [gfph,monoh,caseh] = goal MT.thy 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   108
  "[| x:gfp(f); mono(f); !! y. y:f(gfp(f)) ==> P(y) |] ==> P(x)";
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   109
by (rtac caseh 1);
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   110
by (rtac subsetD 1);
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   111
by (rtac gfp_lemma2 1);
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   112
by (rtac monoh 1);
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   113
by (rtac gfph 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   114
qed "gfp_elim2";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   115
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   116
(* ############################################################ *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   117
(* Expressions                                                  *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   118
(* ############################################################ *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   119
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   120
val e_injs = [e_const_inj, e_var_inj, e_fn_inj, e_fix_inj, e_app_inj];
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   121
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   122
val e_disjs = 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   123
  [ e_disj_const_var, 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   124
    e_disj_const_fn, 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   125
    e_disj_const_fix, 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   126
    e_disj_const_app,
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   127
    e_disj_var_fn, 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   128
    e_disj_var_fix, 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   129
    e_disj_var_app, 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   130
    e_disj_fn_fix, 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   131
    e_disj_fn_app, 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   132
    e_disj_fix_app
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   133
  ];
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   134
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   135
val e_disj_si = e_disjs @ (e_disjs RL [not_sym]);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   136
val e_disj_se = (e_disj_si RL [notE]);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   137
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   138
fun e_ext_cs cs = cs addSIs e_disj_si addSEs e_disj_se addSDs e_injs;
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   139
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   140
(* ############################################################ *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   141
(* Values                                                      *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   142
(* ############################################################ *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   143
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   144
val v_disjs = [v_disj_const_clos];
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   145
val v_disj_si = v_disjs @ (v_disjs RL [not_sym]);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   146
val v_disj_se = (v_disj_si RL [notE]);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   147
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   148
val v_injs = [v_const_inj, v_clos_inj];
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   149
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   150
fun v_ext_cs cs  = cs addSIs v_disj_si addSEs v_disj_se addSDs v_injs;
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   151
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   152
(* ############################################################ *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   153
(* Evaluations                                                  *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   154
(* ############################################################ *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   155
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   156
(* Monotonicity of eval_fun *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   157
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   158
goalw MT.thy [mono_def, eval_fun_def] "mono(eval_fun)";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   159
by infsys_mono_tac;
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   160
qed "eval_fun_mono";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   161
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   162
(* Introduction rules *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   163
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   164
goalw MT.thy [eval_def, eval_rel_def] "ve |- e_const(c) ---> v_const(c)";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   165
by (rtac lfp_intro2 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   166
by (rtac eval_fun_mono 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   167
by (rewtac eval_fun_def);
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   168
by (fast_tac set_cs 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   169
qed "eval_const";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   170
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   171
val prems = goalw MT.thy [eval_def, eval_rel_def] 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   172
  "ev:ve_dom(ve) ==> ve |- e_var(ev) ---> ve_app ve ev";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   173
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   174
by (rtac lfp_intro2 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   175
by (rtac eval_fun_mono 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   176
by (rewtac eval_fun_def);
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   177
by (fast_tac set_cs 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1047
diff changeset
   178
qed "eval_var2";
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   179
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   180
val prems = goalw MT.thy [eval_def, eval_rel_def] 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   181
  "ve |- fn ev => e ---> v_clos(<|ev,e,ve|>)";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   182
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   183
by (rtac lfp_intro2 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   184
by (rtac eval_fun_mono 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   185
by (rewtac eval_fun_def);
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   186
by (fast_tac set_cs 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   187
qed "eval_fn";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   188
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   189
val prems = goalw MT.thy [eval_def, eval_rel_def] 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   190
  " cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   191
\   ve |- fix ev2(ev1) = e ---> v_clos(cl)";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   192
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   193
by (rtac lfp_intro2 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   194
by (rtac eval_fun_mono 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   195
by (rewtac eval_fun_def);
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   196
by (fast_tac set_cs 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   197
qed "eval_fix";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   198
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   199
val prems = goalw MT.thy [eval_def, eval_rel_def]
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   200
  " [| ve |- e1 ---> v_const(c1); ve |- e2 ---> v_const(c2) |] ==> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   201
\   ve |- e1 @ e2 ---> v_const(c_app c1 c2)";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   202
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   203
by (rtac lfp_intro2 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   204
by (rtac eval_fun_mono 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   205
by (rewtac eval_fun_def);
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   206
by (fast_tac set_cs 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   207
qed "eval_app1";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   208
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   209
val prems = goalw MT.thy [eval_def, eval_rel_def] 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   210
  " [|  ve |- e1 ---> v_clos(<|xm,em,vem|>); \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   211
\       ve |- e2 ---> v2; \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   212
\       vem + {xm |-> v2} |- em ---> v \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   213
\   |] ==> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   214
\   ve |- e1 @ e2 ---> v";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   215
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   216
by (rtac lfp_intro2 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   217
by (rtac eval_fun_mono 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   218
by (rewtac eval_fun_def);
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   219
by (fast_tac (set_cs addSIs [disjI2]) 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   220
qed "eval_app2";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   221
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   222
(* Strong elimination, induction on evaluations *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   223
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   224
val prems = goalw MT.thy [eval_def, eval_rel_def]
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   225
  " [| ve |- e ---> v; \
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   226
\      !!ve c. P(((ve,e_const(c)),v_const(c))); \
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   227
\      !!ev ve. ev:ve_dom(ve) ==> P(((ve,e_var(ev)),ve_app ve ev)); \
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   228
\      !!ev ve e. P(((ve,fn ev => e),v_clos(<|ev,e,ve|>))); \
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   229
\      !!ev1 ev2 ve cl e. \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   230
\        cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   231
\        P(((ve,fix ev2(ev1) = e),v_clos(cl))); \
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   232
\      !!ve c1 c2 e1 e2. \
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   233
\        [| P(((ve,e1),v_const(c1))); P(((ve,e2),v_const(c2))) |] ==> \
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   234
\        P(((ve,e1 @ e2),v_const(c_app c1 c2))); \
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   235
\      !!ve vem xm e1 e2 em v v2. \
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   236
\        [|  P(((ve,e1),v_clos(<|xm,em,vem|>))); \
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   237
\            P(((ve,e2),v2)); \
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   238
\            P(((vem + {xm |-> v2},em),v)) \
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   239
\        |] ==> \
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   240
\        P(((ve,e1 @ e2),v)) \
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   241
\   |] ==> \
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   242
\   P(((ve,e),v))";
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   243
by (resolve_tac (prems RL [lfp_ind2]) 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   244
by (rtac eval_fun_mono 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   245
by (rewtac eval_fun_def);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   246
by (dtac CollectD 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   247
by (safe_tac HOL_cs);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   248
by (ALLGOALS (resolve_tac prems));
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   249
by (ALLGOALS (fast_tac set_cs));
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   250
qed "eval_ind0";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   251
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   252
val prems = goal MT.thy 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   253
  " [| ve |- e ---> v; \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   254
\      !!ve c. P ve (e_const c) (v_const c); \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   255
\      !!ev ve. ev:ve_dom(ve) ==> P ve (e_var ev) (ve_app ve ev); \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   256
\      !!ev ve e. P ve (fn ev => e) (v_clos <|ev,e,ve|>); \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   257
\      !!ev1 ev2 ve cl e. \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   258
\        cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   259
\        P ve (fix ev2(ev1) = e) (v_clos cl); \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   260
\      !!ve c1 c2 e1 e2. \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   261
\        [| P ve e1 (v_const c1); P ve e2 (v_const c2) |] ==> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   262
\        P ve (e1 @ e2) (v_const(c_app c1 c2)); \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   263
\      !!ve vem evm e1 e2 em v v2. \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   264
\        [|  P ve e1 (v_clos <|evm,em,vem|>); \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   265
\            P ve e2 v2; \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   266
\            P (vem + {evm |-> v2}) em v \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   267
\        |] ==> P ve (e1 @ e2) v \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   268
\   |] ==> P ve e v";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   269
by (res_inst_tac [("P","P")] infsys_pp2 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   270
by (rtac eval_ind0 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   271
by (ALLGOALS (rtac infsys_pp1));
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   272
by (ALLGOALS (resolve_tac prems));
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   273
by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   274
qed "eval_ind";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   275
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   276
(* ############################################################ *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   277
(* Elaborations                                                 *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   278
(* ############################################################ *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   279
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   280
goalw MT.thy [mono_def, elab_fun_def] "mono(elab_fun)";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   281
by infsys_mono_tac;
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   282
qed "elab_fun_mono";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   283
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   284
(* Introduction rules *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   285
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   286
val prems = goalw MT.thy [elab_def, elab_rel_def] 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   287
  "c isof ty ==> te |- e_const(c) ===> ty";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   288
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   289
by (rtac lfp_intro2 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   290
by (rtac elab_fun_mono 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   291
by (rewtac elab_fun_def);
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   292
by (fast_tac set_cs 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   293
qed "elab_const";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   294
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   295
val prems = goalw MT.thy [elab_def, elab_rel_def] 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   296
  "x:te_dom(te) ==> te |- e_var(x) ===> te_app te x";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   297
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   298
by (rtac lfp_intro2 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   299
by (rtac elab_fun_mono 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   300
by (rewtac elab_fun_def);
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   301
by (fast_tac set_cs 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   302
qed "elab_var";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   303
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   304
val prems = goalw MT.thy [elab_def, elab_rel_def] 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   305
  "te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   306
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   307
by (rtac lfp_intro2 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   308
by (rtac elab_fun_mono 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   309
by (rewtac elab_fun_def);
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   310
by (fast_tac set_cs 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   311
qed "elab_fn";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   312
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   313
val prems = goalw MT.thy [elab_def, elab_rel_def]
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   314
  " te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   315
\   te |- fix f(x) = e ===> ty1->ty2";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   316
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   317
by (rtac lfp_intro2 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   318
by (rtac elab_fun_mono 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   319
by (rewtac elab_fun_def);
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   320
by (fast_tac set_cs 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   321
qed "elab_fix";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   322
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   323
val prems = goalw MT.thy [elab_def, elab_rel_def] 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   324
  " [| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   325
\   te |- e1 @ e2 ===> ty2";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   326
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   327
by (rtac lfp_intro2 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   328
by (rtac elab_fun_mono 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   329
by (rewtac elab_fun_def);
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   330
by (fast_tac (set_cs addSIs [disjI2]) 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   331
qed "elab_app";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   332
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   333
(* Strong elimination, induction on elaborations *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   334
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   335
val prems = goalw MT.thy [elab_def, elab_rel_def]
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   336
  " [| te |- e ===> t; \
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   337
\      !!te c t. c isof t ==> P(((te,e_const(c)),t)); \
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   338
\      !!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x)); \
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   339
\      !!te x e t1 t2. \
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   340
\        [| te + {x |=> t1} |- e ===> t2; P(((te + {x |=> t1},e),t2)) |] ==> \
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   341
\        P(((te,fn x => e),t1->t2)); \
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   342
\      !!te f x e t1 t2. \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   343
\        [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2; \
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   344
\           P(((te + {f |=> t1->t2} + {x |=> t1},e),t2)) \
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   345
\        |] ==> \
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   346
\        P(((te,fix f(x) = e),t1->t2)); \
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   347
\      !!te e1 e2 t1 t2. \
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   348
\        [| te |- e1 ===> t1->t2; P(((te,e1),t1->t2)); \
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   349
\           te |- e2 ===> t1; P(((te,e2),t1)) \
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   350
\        |] ==> \
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   351
\        P(((te,e1 @ e2),t2)) \
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   352
\   |] ==> \
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   353
\   P(((te,e),t))";
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   354
by (resolve_tac (prems RL [lfp_ind2]) 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   355
by (rtac elab_fun_mono 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   356
by (rewtac elab_fun_def);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   357
by (dtac CollectD 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   358
by (safe_tac HOL_cs);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   359
by (ALLGOALS (resolve_tac prems));
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   360
by (ALLGOALS (fast_tac set_cs));
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   361
qed "elab_ind0";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   362
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   363
val prems = goal MT.thy
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   364
  " [| te |- e ===> t; \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   365
\       !!te c t. c isof t ==> P te (e_const c) t; \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   366
\      !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x); \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   367
\      !!te x e t1 t2. \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   368
\        [| te + {x |=> t1} |- e ===> t2; P (te + {x |=> t1}) e t2 |] ==> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   369
\        P te (fn x => e) (t1->t2); \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   370
\      !!te f x e t1 t2. \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   371
\        [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2; \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   372
\           P (te + {f |=> t1->t2} + {x |=> t1}) e t2 \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   373
\        |] ==> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   374
\        P te (fix f(x) = e) (t1->t2); \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   375
\      !!te e1 e2 t1 t2. \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   376
\        [| te |- e1 ===> t1->t2; P te e1 (t1->t2); \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   377
\           te |- e2 ===> t1; P te e2 t1 \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   378
\        |] ==> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   379
\        P te (e1 @ e2) t2 \ 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   380
\   |] ==> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   381
\   P te e t";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   382
by (res_inst_tac [("P","P")] infsys_pp2 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   383
by (rtac elab_ind0 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   384
by (ALLGOALS (rtac infsys_pp1));
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   385
by (ALLGOALS (resolve_tac prems));
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   386
by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   387
qed "elab_ind";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   388
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   389
(* Weak elimination, case analysis on elaborations *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   390
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   391
val prems = goalw MT.thy [elab_def, elab_rel_def]
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   392
  " [| te |- e ===> t; \
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   393
\      !!te c t. c isof t ==> P(((te,e_const(c)),t)); \
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   394
\      !!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x)); \
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   395
\      !!te x e t1 t2. \
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   396
\        te + {x |=> t1} |- e ===> t2 ==> P(((te,fn x => e),t1->t2)); \
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   397
\      !!te f x e t1 t2. \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   398
\        te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==> \
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   399
\        P(((te,fix f(x) = e),t1->t2)); \
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   400
\      !!te e1 e2 t1 t2. \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   401
\        [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> \
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   402
\        P(((te,e1 @ e2),t2)) \
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   403
\   |] ==> \
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   404
\   P(((te,e),t))";
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   405
by (resolve_tac (prems RL [lfp_elim2]) 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   406
by (rtac elab_fun_mono 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   407
by (rewtac elab_fun_def);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   408
by (dtac CollectD 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   409
by (safe_tac HOL_cs);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   410
by (ALLGOALS (resolve_tac prems));
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   411
by (ALLGOALS (fast_tac set_cs));
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   412
qed "elab_elim0";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   413
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   414
val prems = goal MT.thy
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   415
  " [| te |- e ===> t; \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   416
\       !!te c t. c isof t ==> P te (e_const c) t; \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   417
\      !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x); \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   418
\      !!te x e t1 t2. \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   419
\        te + {x |=> t1} |- e ===> t2 ==> P te (fn x => e) (t1->t2); \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   420
\      !!te f x e t1 t2. \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   421
\        te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   422
\        P te (fix f(x) = e) (t1->t2); \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   423
\      !!te e1 e2 t1 t2. \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   424
\        [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   425
\        P te (e1 @ e2) t2 \ 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   426
\   |] ==> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   427
\   P te e t";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   428
by (res_inst_tac [("P","P")] infsys_pp2 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   429
by (rtac elab_elim0 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   430
by (ALLGOALS (rtac infsys_pp1));
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   431
by (ALLGOALS (resolve_tac prems));
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   432
by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   433
qed "elab_elim";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   434
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   435
(* Elimination rules for each expression *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   436
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   437
fun elab_e_elim_tac p = 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   438
  ( (rtac elab_elim 1) THEN 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   439
    (resolve_tac p 1) THEN 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   440
    (REPEAT (fast_tac (e_ext_cs HOL_cs) 1))
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   441
  );
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   442
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   443
val prems = goal MT.thy "te |- e ===> t ==> (e = e_const(c) --> c isof t)";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   444
by (elab_e_elim_tac prems);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   445
qed "elab_const_elim_lem";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   446
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   447
val prems = goal MT.thy "te |- e_const(c) ===> t ==> c isof t";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   448
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   449
by (dtac elab_const_elim_lem 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   450
by (fast_tac prop_cs 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   451
qed "elab_const_elim";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   452
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   453
val prems = goal MT.thy 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   454
  "te |- e ===> t ==> (e = e_var(x) --> t=te_app te x & x:te_dom(te))";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   455
by (elab_e_elim_tac prems);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   456
qed "elab_var_elim_lem";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   457
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   458
val prems = goal MT.thy 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   459
  "te |- e_var(ev) ===> t ==> t=te_app te ev & ev : te_dom(te)";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   460
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   461
by (dtac elab_var_elim_lem 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   462
by (fast_tac prop_cs 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   463
qed "elab_var_elim";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   464
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   465
val prems = goal MT.thy 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   466
  " te |- e ===> t ==> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   467
\   ( e = fn x1 => e1 --> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   468
\     (? t1 t2.t=t_fun t1 t2 & te + {x1 |=> t1} |- e1 ===> t2) \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   469
\   )";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   470
by (elab_e_elim_tac prems);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   471
qed "elab_fn_elim_lem";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   472
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   473
val prems = goal MT.thy 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   474
  " te |- fn x1 => e1 ===> t ==> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   475
\   (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   476
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   477
by (dtac elab_fn_elim_lem 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   478
by (fast_tac prop_cs 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   479
qed "elab_fn_elim";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   480
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   481
val prems = goal MT.thy 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   482
  " te |- e ===> t ==> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   483
\   (e = fix f(x) = e1 --> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   484
\   (? t1 t2. t=t1->t2 & te + {f |=> t1->t2} + {x |=> t1} |- e1 ===> t2))"; 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   485
by (elab_e_elim_tac prems);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   486
qed "elab_fix_elim_lem";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   487
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   488
val prems = goal MT.thy 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   489
  " te |- fix ev1(ev2) = e1 ===> t ==> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   490
\   (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   491
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   492
by (dtac elab_fix_elim_lem 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   493
by (fast_tac prop_cs 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   494
qed "elab_fix_elim";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   495
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   496
val prems = goal MT.thy 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   497
  " te |- e ===> t2 ==> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   498
\   (e = e1 @ e2 --> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1))"; 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   499
by (elab_e_elim_tac prems);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   500
qed "elab_app_elim_lem";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   501
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1047
diff changeset
   502
val prems = goal MT.thy
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1047
diff changeset
   503
 "te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)"; 
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   504
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   505
by (dtac elab_app_elim_lem 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   506
by (fast_tac prop_cs 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   507
qed "elab_app_elim";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   508
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   509
(* ############################################################ *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   510
(* The extended correspondence relation                       *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   511
(* ############################################################ *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   512
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   513
(* Monotonicity of hasty_fun *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   514
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   515
goalw MT.thy [mono_def,MT.hasty_fun_def] "mono(hasty_fun)";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   516
by infsys_mono_tac;
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   517
bind_thm("mono_hasty_fun",  result());
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   518
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   519
(* 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   520
  Because hasty_rel has been defined as the greatest fixpoint of hasty_fun it 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   521
  enjoys two strong indtroduction (co-induction) rules and an elimination rule.
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   522
*)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   523
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   524
(* First strong indtroduction (co-induction) rule for hasty_rel *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   525
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1047
diff changeset
   526
val prems =
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1047
diff changeset
   527
  goalw MT.thy [hasty_rel_def] "c isof t ==> (v_const(c),t) : hasty_rel";
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   528
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   529
by (rtac gfp_coind2 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   530
by (rewtac MT.hasty_fun_def);
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   531
by (rtac CollectI 1);
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   532
by (rtac disjI1 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   533
by (fast_tac HOL_cs 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   534
by (rtac mono_hasty_fun 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   535
qed "hasty_rel_const_coind";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   536
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   537
(* Second strong introduction (co-induction) rule for hasty_rel *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   538
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   539
val prems = goalw MT.thy [hasty_rel_def]
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   540
  " [|  te |- fn ev => e ===> t; \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   541
\       ve_dom(ve) = te_dom(te); \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   542
\       ! ev1. \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   543
\         ev1:ve_dom(ve) --> \
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   544
\         (ve_app ve ev1,te_app te ev1) : {(v_clos(<|ev,e,ve|>),t)} Un hasty_rel \
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   545
\   |] ==> \
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   546
\   (v_clos(<|ev,e,ve|>),t) : hasty_rel";
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   547
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   548
by (rtac gfp_coind2 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   549
by (rewtac hasty_fun_def);
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   550
by (rtac CollectI 1);
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   551
by (rtac disjI2 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   552
by (fast_tac HOL_cs 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   553
by (rtac mono_hasty_fun 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   554
qed "hasty_rel_clos_coind";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   555
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   556
(* Elimination rule for hasty_rel *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   557
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   558
val prems = goalw MT.thy [hasty_rel_def]
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   559
  " [| !! c t.c isof t ==> P((v_const(c),t)); \
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   560
\      !! te ev e t ve. \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   561
\        [| te |- fn ev => e ===> t; \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   562
\           ve_dom(ve) = te_dom(te); \
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   563
\           !ev1.ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel \
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   564
\        |] ==> P((v_clos(<|ev,e,ve|>),t)); \
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   565
\      (v,t) : hasty_rel \
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   566
\   |] ==> P((v,t))";
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   567
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   568
by (etac gfp_elim2 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   569
by (rtac mono_hasty_fun 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   570
by (rewtac hasty_fun_def);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   571
by (dtac CollectD 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   572
by (fold_goals_tac [hasty_fun_def]);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   573
by (safe_tac HOL_cs);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   574
by (ALLGOALS (resolve_tac prems));
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   575
by (ALLGOALS (fast_tac set_cs));
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   576
qed "hasty_rel_elim0";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   577
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   578
val prems = goal MT.thy 
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   579
  " [| (v,t) : hasty_rel; \
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   580
\      !! c t.c isof t ==> P (v_const c) t; \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   581
\      !! te ev e t ve. \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   582
\        [| te |- fn ev => e ===> t; \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   583
\           ve_dom(ve) = te_dom(te); \
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 969
diff changeset
   584
\           !ev1.ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel \
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   585
\        |] ==> P (v_clos <|ev,e,ve|>) t \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   586
\   |] ==> P v t";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   587
by (res_inst_tac [("P","P")] infsys_p2 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   588
by (rtac hasty_rel_elim0 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   589
by (ALLGOALS (rtac infsys_p1));
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   590
by (ALLGOALS (resolve_tac prems));
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   591
by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_p2 1)));
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   592
qed "hasty_rel_elim";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   593
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   594
(* Introduction rules for hasty *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   595
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   596
val prems = goalw MT.thy [hasty_def] "c isof t ==> v_const(c) hasty t";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   597
by (resolve_tac (prems RL [hasty_rel_const_coind]) 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   598
qed "hasty_const";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   599
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   600
val prems = goalw MT.thy [hasty_def,hasty_env_def] 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   601
  "te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   602
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   603
by (rtac hasty_rel_clos_coind 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   604
by (ALLGOALS (fast_tac set_cs));
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   605
qed "hasty_clos";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   606
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   607
(* Elimination on constants for hasty *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   608
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   609
val prems = goalw MT.thy [hasty_def] 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   610
  "v hasty t ==> (!c.(v = v_const(c) --> c isof t))";  
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   611
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   612
by (rtac hasty_rel_elim 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   613
by (ALLGOALS (fast_tac (v_ext_cs HOL_cs)));
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   614
qed "hasty_elim_const_lem";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   615
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   616
val prems = goal MT.thy "v_const(c) hasty t ==> c isof t";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   617
by (cut_facts_tac (prems RL [hasty_elim_const_lem]) 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   618
by (fast_tac HOL_cs 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   619
qed "hasty_elim_const";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   620
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   621
(* Elimination on closures for hasty *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   622
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   623
val prems = goalw MT.thy [hasty_env_def,hasty_def] 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   624
  " v hasty t ==> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   625
\   ! x e ve. \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   626
\     v=v_clos(<|x,e,ve|>) --> (? te.te |- fn x => e ===> t & ve hastyenv te)";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   627
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   628
by (rtac hasty_rel_elim 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   629
by (ALLGOALS (fast_tac (v_ext_cs HOL_cs)));
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   630
qed "hasty_elim_clos_lem";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   631
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   632
val prems = goal MT.thy 
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1047
diff changeset
   633
  "v_clos(<|ev,e,ve|>) hasty t ==> ? te.te |- fn ev => e ===>\
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1047
diff changeset
   634
  \t & ve hastyenv te ";
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   635
by (cut_facts_tac (prems RL [hasty_elim_clos_lem]) 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   636
by (fast_tac HOL_cs 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   637
qed "hasty_elim_clos";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   638
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   639
(* ############################################################ *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   640
(* The pointwise extension of hasty to environments             *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   641
(* ############################################################ *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   642
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   643
goal MT.thy
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   644
  "!!ve. [| ve hastyenv te; v hasty t |] ==> \
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   645
\        ve + {ev |-> v} hastyenv te + {ev |=> t}";
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   646
by (rewtac hasty_env_def);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1047
diff changeset
   647
by (asm_full_simp_tac (!simpset delsimps mem_simps
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1047
diff changeset
   648
                                addsimps [ve_dom_owr, te_dom_owr]) 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   649
by (safe_tac HOL_cs);
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   650
by (excluded_middle_tac "ev=x" 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1047
diff changeset
   651
by (asm_full_simp_tac (!simpset addsimps [ve_app_owr2, te_app_owr2]) 1);
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   652
by (fast_tac set_cs 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1047
diff changeset
   653
by (asm_simp_tac (!simpset addsimps [ve_app_owr1, te_app_owr1]) 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   654
qed "hasty_env1";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   655
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   656
(* ############################################################ *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   657
(* The Consistency theorem                                      *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   658
(* ############################################################ *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   659
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   660
val prems = goal MT.thy 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   661
  "[| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   662
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   663
by (dtac elab_const_elim 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   664
by (etac hasty_const 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   665
qed "consistency_const";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   666
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   667
val prems = goalw MT.thy [hasty_env_def]
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   668
  " [| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   669
\   ve_app ve ev hasty t";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   670
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   671
by (dtac elab_var_elim 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   672
by (fast_tac HOL_cs 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   673
qed "consistency_var";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   674
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   675
val prems = goal MT.thy
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   676
  " [| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   677
\   v_clos(<| ev, e, ve |>) hasty t";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   678
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   679
by (rtac hasty_clos 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   680
by (fast_tac prop_cs 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   681
qed "consistency_fn";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   682
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   683
val prems = goalw MT.thy [hasty_env_def,hasty_def]
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   684
  " [| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>; \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   685
\      ve hastyenv te ; \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   686
\      te |- fix ev2  ev1  = e ===> t \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   687
\   |] ==> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   688
\   v_clos(cl) hasty t";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   689
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   690
by (dtac elab_fix_elim 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   691
by (safe_tac HOL_cs);
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   692
(*Do a single unfolding of cl*)
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   693
by ((forward_tac [ssubst] 1) THEN (assume_tac 2));
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   694
by (rtac hasty_rel_clos_coind 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   695
by (etac elab_fn 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1047
diff changeset
   696
by (asm_simp_tac (!simpset addsimps [ve_dom_owr, te_dom_owr]) 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   697
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1047
diff changeset
   698
by (asm_simp_tac (!simpset delsimps mem_simps addsimps [ve_dom_owr]) 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   699
by (safe_tac HOL_cs);
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   700
by (excluded_middle_tac "ev2=ev1a" 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1047
diff changeset
   701
by (asm_full_simp_tac (!simpset addsimps [ve_app_owr2, te_app_owr2]) 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   702
by (fast_tac set_cs 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   703
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1047
diff changeset
   704
by (asm_simp_tac (!simpset delsimps mem_simps
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1047
diff changeset
   705
                           addsimps [ve_app_owr1, te_app_owr1]) 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   706
by (hyp_subst_tac 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   707
by (etac subst 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   708
by (fast_tac set_cs 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   709
qed "consistency_fix";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   710
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   711
val prems = goal MT.thy 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   712
  " [| ! t te. ve hastyenv te  --> te |- e1 ===> t --> v_const(c1) hasty t; \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   713
\      ! t te. ve hastyenv te  --> te |- e2 ===> t --> v_const(c2) hasty t; \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   714
\      ve hastyenv te ; te |- e1 @ e2 ===> t \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   715
\   |] ==> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   716
\   v_const(c_app c1 c2) hasty t";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   717
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   718
by (dtac elab_app_elim 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   719
by (safe_tac HOL_cs);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   720
by (rtac hasty_const 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   721
by (rtac isof_app 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   722
by (rtac hasty_elim_const 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   723
by (fast_tac HOL_cs 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   724
by (rtac hasty_elim_const 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   725
by (fast_tac HOL_cs 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   726
qed "consistency_app1";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   727
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   728
val prems = goal MT.thy 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   729
  " [| ! t te. \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   730
\        ve hastyenv te  --> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   731
\        te |- e1 ===> t --> v_clos(<|evm, em, vem|>) hasty t; \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   732
\      ! t te. ve hastyenv te  --> te |- e2 ===> t --> v2 hasty t; \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   733
\      ! t te. \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   734
\        vem + { evm |-> v2 } hastyenv te  --> te |- em ===> t --> v hasty t; \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   735
\      ve hastyenv te ; \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   736
\      te |- e1 @ e2 ===> t \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   737
\   |] ==> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   738
\   v hasty t";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   739
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   740
by (dtac elab_app_elim 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   741
by (safe_tac HOL_cs);
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   742
by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   743
by (assume_tac 1);
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   744
by (etac impE 1);
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   745
by (assume_tac 1);
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   746
by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   747
by (assume_tac 1);
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   748
by (etac impE 1);
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   749
by (assume_tac 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   750
by (dtac hasty_elim_clos 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   751
by (safe_tac HOL_cs);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   752
by (dtac elab_fn_elim 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   753
by (safe_tac HOL_cs);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   754
by (dtac t_fun_inj 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   755
by (safe_tac prop_cs);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   756
by ((dtac hasty_env1 1) THEN (assume_tac 1) THEN (fast_tac HOL_cs 1));
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   757
qed "consistency_app2";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   758
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   759
val [major] = goal MT.thy 
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   760
  "ve |- e ---> v ==> \
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   761
\  (! t te. ve hastyenv te --> te |- e ===> t --> v hasty t)";
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   762
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   763
(* Proof by induction on the structure of evaluations *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   764
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   765
by (rtac (major RS eval_ind) 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   766
by (safe_tac HOL_cs);
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   767
by (DEPTH_SOLVE 
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   768
    (ares_tac [consistency_const, consistency_var, consistency_fn,
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   769
	       consistency_fix, consistency_app1, consistency_app2] 1));
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   770
qed "consistency";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   771
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   772
(* ############################################################ *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   773
(* The Basic Consistency theorem                                *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   774
(* ############################################################ *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   775
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   776
val prems = goalw MT.thy [isof_env_def,hasty_env_def] 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   777
  "ve isofenv te ==> ve hastyenv te";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   778
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   779
by (safe_tac HOL_cs);
1047
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   780
by (etac allE 1);
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   781
by (etac impE 1);
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   782
by (assume_tac 1);
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   783
by (etac exE 1);
5133479a37cf Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents: 972
diff changeset
   784
by (etac conjE 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   785
by (dtac hasty_const 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1047
diff changeset
   786
by (Asm_simp_tac 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   787
qed "basic_consistency_lem";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   788
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   789
val prems = goal MT.thy
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   790
  "[| ve isofenv te; ve |- e ---> v_const(c); te |- e ===> t |] ==> c isof t";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   791
by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   792
by (rtac hasty_elim_const 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   793
by (dtac consistency 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   794
by (fast_tac (HOL_cs addSIs [basic_consistency_lem]) 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   795
qed "basic_consistency";