src/HOL/ex/MT.ML
changeset 5278 a903b66822e2
parent 5227 e5a6ace920a0
child 7499 23e090051cb8
     1.1 --- a/src/HOL/ex/MT.ML	Thu Aug 06 15:47:26 1998 +0200
     1.2 +++ b/src/HOL/ex/MT.ML	Thu Aug 06 15:48:13 1998 +0200
     1.3 @@ -439,8 +439,7 @@
     1.4  by (elab_e_elim_tac prems);
     1.5  qed "elab_fn_elim_lem";
     1.6  
     1.7 -Goal 
     1.8 -  " te |- fn x1 => e1 ===> t ==> \
     1.9 +Goal " te |- fn x1 => e1 ===> t ==> \
    1.10  \   (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)";
    1.11  by (dtac elab_fn_elim_lem 1);
    1.12  by (Blast_tac 1);
    1.13 @@ -453,8 +452,7 @@
    1.14  by (elab_e_elim_tac prems);
    1.15  qed "elab_fix_elim_lem";
    1.16  
    1.17 -Goal 
    1.18 -  " te |- fix ev1(ev2) = e1 ===> t ==> \
    1.19 +Goal " te |- fix ev1(ev2) = e1 ===> t ==> \
    1.20  \   (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)";
    1.21  by (dtac elab_fix_elim_lem 1);
    1.22  by (Blast_tac 1);
    1.23 @@ -466,8 +464,7 @@
    1.24  by (elab_e_elim_tac prems);
    1.25  qed "elab_app_elim_lem";
    1.26  
    1.27 -Goal
    1.28 - "te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)"; 
    1.29 +Goal "te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)"; 
    1.30  by (dtac elab_app_elim_lem 1);
    1.31  by (Blast_tac 1);
    1.32  qed "elab_app_elim";
    1.33 @@ -589,8 +586,7 @@
    1.34  by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
    1.35  qed "hasty_elim_clos_lem";
    1.36  
    1.37 -Goal 
    1.38 -  "v_clos(<|ev,e,ve|>) hasty t ==>  \
    1.39 +Goal "v_clos(<|ev,e,ve|>) hasty t ==>  \
    1.40  \       ? te. te |- fn ev => e ===> t & ve hastyenv te ";
    1.41  by (dtac hasty_elim_clos_lem 1);
    1.42  by (Blast_tac 1);
    1.43 @@ -600,8 +596,7 @@
    1.44  (* The pointwise extension of hasty to environments             *)
    1.45  (* ############################################################ *)
    1.46  
    1.47 -Goal
    1.48 -  "[| ve hastyenv te; v hasty t |] ==> \
    1.49 +Goal "[| ve hastyenv te; v hasty t |] ==> \
    1.50  \        ve + {ev |-> v} hastyenv te + {ev |=> t}";
    1.51  by (rewtac hasty_env_def);
    1.52  by (asm_full_simp_tac (simpset() delsimps mem_simps
    1.53 @@ -617,8 +612,7 @@
    1.54  (* The Consistency theorem                                      *)
    1.55  (* ############################################################ *)
    1.56  
    1.57 -Goal 
    1.58 -  "[| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t";
    1.59 +Goal "[| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t";
    1.60  by (dtac elab_const_elim 1);
    1.61  by (etac hasty_const 1);
    1.62  qed "consistency_const";
    1.63 @@ -630,8 +624,7 @@
    1.64  by (Blast_tac 1);
    1.65  qed "consistency_var";
    1.66  
    1.67 -Goal
    1.68 -  "[| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
    1.69 +Goal "[| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
    1.70  \       v_clos(<| ev, e, ve |>) hasty t";
    1.71  by (rtac hasty_clos 1);
    1.72  by (Blast_tac 1);
    1.73 @@ -664,8 +657,7 @@
    1.74  by (Blast_tac 1);
    1.75  qed "consistency_fix";
    1.76  
    1.77 -Goal 
    1.78 -  "[| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t;\
    1.79 +Goal "[| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t;\
    1.80  \      ! t te. ve hastyenv te  --> te |- e2 ===> t --> v_const(c2) hasty t; \
    1.81  \      ve hastyenv te ; te |- e1 @ e2 ===> t \
    1.82  \   |] ==> \
    1.83 @@ -680,8 +672,7 @@
    1.84  by (Blast_tac 1);
    1.85  qed "consistency_app1";
    1.86  
    1.87 -Goal 
    1.88 -  "[| ! t te. \
    1.89 +Goal "[| ! t te. \
    1.90  \        ve hastyenv te  --> \
    1.91  \        te |- e1 ===> t --> v_clos(<|evm, em, vem|>) hasty t; \
    1.92  \      ! t te. ve hastyenv te  --> te |- e2 ===> t --> v2 hasty t; \
    1.93 @@ -707,8 +698,7 @@
    1.94  by (blast_tac (claset() addIs [hasty_env1] addSDs [t_fun_inj]) 1);
    1.95  qed "consistency_app2";
    1.96  
    1.97 -Goal
    1.98 -  "ve |- e ---> v ==> \
    1.99 +Goal "ve |- e ---> v ==> \
   1.100  \  (! t te. ve hastyenv te --> te |- e ===> t --> v hasty t)";
   1.101  
   1.102  (* Proof by induction on the structure of evaluations *)
   1.103 @@ -736,8 +726,7 @@
   1.104  by (Asm_simp_tac 1);
   1.105  qed "basic_consistency_lem";
   1.106  
   1.107 -Goal
   1.108 -  "[| ve isofenv te; ve |- e ---> v_const(c); te |- e ===> t |] ==> c isof t";
   1.109 +Goal "[| ve isofenv te; ve |- e ---> v_const(c); te |- e ===> t |] ==> c isof t";
   1.110  by (rtac hasty_elim_const 1);
   1.111  by (dtac consistency 1);
   1.112  by (blast_tac (claset() addSIs [basic_consistency_lem]) 1);