src/HOL/ex/MT.ML
changeset 972 e61b058d58d2
parent 969 b051e2fc2e34
child 1047 5133479a37cf
     1.1 --- a/src/HOL/ex/MT.ML	Thu Mar 23 15:39:13 1995 +0100
     1.2 +++ b/src/HOL/ex/MT.ML	Fri Mar 24 12:30:35 1995 +0100
     1.3 @@ -45,13 +45,13 @@
     1.4        (REPEAT (etac exE 1)) THEN (REPEAT (rtac exI 1)) THEN (fast_tac set_cs 1)
     1.5      );
     1.6  
     1.7 -val prems = goal MT.thy "P a b ==> P (fst <a,b>) (snd <a,b>)";
     1.8 +val prems = goal MT.thy "P a b ==> P (fst (a,b)) (snd (a,b))";
     1.9  by (rtac (fst_conv RS ssubst) 1);
    1.10  by (rtac (snd_conv RS ssubst) 1);
    1.11  by (resolve_tac prems 1);
    1.12  qed "infsys_p1";
    1.13  
    1.14 -val prems = goal MT.thy "P (fst <a,b>) (snd <a,b>) ==> P a b";
    1.15 +val prems = goal MT.thy "P (fst (a,b)) (snd (a,b)) ==> P a b";
    1.16  by (cut_facts_tac prems 1);
    1.17  by (dtac (fst_conv RS subst) 1);
    1.18  by (dtac (snd_conv RS subst) 1);
    1.19 @@ -59,7 +59,7 @@
    1.20  qed "infsys_p2";
    1.21  
    1.22  val prems = goal MT.thy 
    1.23 -  "P a b c ==> P (fst(fst <<a,b>,c>)) (snd(fst <<a,b>,c>)) (snd <<a,b>,c>)";
    1.24 +  "P a b c ==> P (fst(fst ((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c))";
    1.25  by (rtac (fst_conv RS ssubst) 1);
    1.26  by (rtac (fst_conv RS ssubst) 1);
    1.27  by (rtac (snd_conv RS ssubst) 1);
    1.28 @@ -68,7 +68,7 @@
    1.29  qed "infsys_pp1";
    1.30  
    1.31  val prems = goal MT.thy 
    1.32 -  "P (fst(fst <<a,b>,c>)) (snd(fst <<a,b>,c>)) (snd <<a,b>,c>) ==> P a b c";
    1.33 +  "P (fst(fst ((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c)) ==> P a b c";
    1.34  by (cut_facts_tac prems 1);
    1.35  by (dtac (fst_conv RS subst) 1);
    1.36  by (dtac (fst_conv RS subst) 1);
    1.37 @@ -240,23 +240,23 @@
    1.38  
    1.39  val prems = goalw MT.thy [eval_def, eval_rel_def]
    1.40    " [| ve |- e ---> v; \
    1.41 -\      !!ve c. P(<<ve,e_const(c)>,v_const(c)>); \
    1.42 -\      !!ev ve. ev:ve_dom(ve) ==> P(<<ve,e_var(ev)>,ve_app ve ev>); \
    1.43 -\      !!ev ve e. P(<<ve,fn ev => e>,v_clos(<|ev,e,ve|>)>); \
    1.44 +\      !!ve c. P(((ve,e_const(c)),v_const(c))); \
    1.45 +\      !!ev ve. ev:ve_dom(ve) ==> P(((ve,e_var(ev)),ve_app ve ev)); \
    1.46 +\      !!ev ve e. P(((ve,fn ev => e),v_clos(<|ev,e,ve|>))); \
    1.47  \      !!ev1 ev2 ve cl e. \
    1.48  \        cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
    1.49 -\        P(<<ve,fix ev2(ev1) = e>,v_clos(cl)>); \
    1.50 +\        P(((ve,fix ev2(ev1) = e),v_clos(cl))); \
    1.51  \      !!ve c1 c2 e1 e2. \
    1.52 -\        [| P(<<ve,e1>,v_const(c1)>); P(<<ve,e2>,v_const(c2)>) |] ==> \
    1.53 -\        P(<<ve,e1 @ e2>,v_const(c_app c1 c2)>); \
    1.54 +\        [| P(((ve,e1),v_const(c1))); P(((ve,e2),v_const(c2))) |] ==> \
    1.55 +\        P(((ve,e1 @ e2),v_const(c_app c1 c2))); \
    1.56  \      !!ve vem xm e1 e2 em v v2. \
    1.57 -\        [|  P(<<ve,e1>,v_clos(<|xm,em,vem|>)>); \
    1.58 -\            P(<<ve,e2>,v2>); \
    1.59 -\            P(<<vem + {xm |-> v2},em>,v>) \
    1.60 +\        [|  P(((ve,e1),v_clos(<|xm,em,vem|>))); \
    1.61 +\            P(((ve,e2),v2)); \
    1.62 +\            P(((vem + {xm |-> v2},em),v)) \
    1.63  \        |] ==> \
    1.64 -\        P(<<ve,e1 @ e2>,v>) \
    1.65 +\        P(((ve,e1 @ e2),v)) \
    1.66  \   |] ==> \
    1.67 -\   P(<<ve,e>,v>)";
    1.68 +\   P(((ve,e),v))";
    1.69  by (resolve_tac (prems RL [lfp_ind2]) 1);
    1.70  by (rtac eval_fun_mono 1);
    1.71  by (rewtac eval_fun_def);
    1.72 @@ -356,23 +356,23 @@
    1.73  
    1.74  val prems = goalw MT.thy [elab_def, elab_rel_def]
    1.75    " [| te |- e ===> t; \
    1.76 -\      !!te c t. c isof t ==> P(<<te,e_const(c)>,t>); \
    1.77 -\      !!te x. x:te_dom(te) ==> P(<<te,e_var(x)>,te_app te x>); \
    1.78 +\      !!te c t. c isof t ==> P(((te,e_const(c)),t)); \
    1.79 +\      !!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x)); \
    1.80  \      !!te x e t1 t2. \
    1.81 -\        [| te + {x |=> t1} |- e ===> t2; P(<<te + {x |=> t1},e>,t2>) |] ==> \
    1.82 -\        P(<<te,fn x => e>,t1->t2>); \
    1.83 +\        [| te + {x |=> t1} |- e ===> t2; P(((te + {x |=> t1},e),t2)) |] ==> \
    1.84 +\        P(((te,fn x => e),t1->t2)); \
    1.85  \      !!te f x e t1 t2. \
    1.86  \        [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2; \
    1.87 -\           P(<<te + {f |=> t1->t2} + {x |=> t1},e>,t2>) \
    1.88 +\           P(((te + {f |=> t1->t2} + {x |=> t1},e),t2)) \
    1.89  \        |] ==> \
    1.90 -\        P(<<te,fix f(x) = e>,t1->t2>); \
    1.91 +\        P(((te,fix f(x) = e),t1->t2)); \
    1.92  \      !!te e1 e2 t1 t2. \
    1.93 -\        [| te |- e1 ===> t1->t2; P(<<te,e1>,t1->t2>); \
    1.94 -\           te |- e2 ===> t1; P(<<te,e2>,t1>) \
    1.95 +\        [| te |- e1 ===> t1->t2; P(((te,e1),t1->t2)); \
    1.96 +\           te |- e2 ===> t1; P(((te,e2),t1)) \
    1.97  \        |] ==> \
    1.98 -\        P(<<te,e1 @ e2>,t2>) \
    1.99 +\        P(((te,e1 @ e2),t2)) \
   1.100  \   |] ==> \
   1.101 -\   P(<<te,e>,t>)";
   1.102 +\   P(((te,e),t))";
   1.103  by (resolve_tac (prems RL [lfp_ind2]) 1);
   1.104  by (rtac elab_fun_mono 1);
   1.105  by (rewtac elab_fun_def);
   1.106 @@ -412,18 +412,18 @@
   1.107  
   1.108  val prems = goalw MT.thy [elab_def, elab_rel_def]
   1.109    " [| te |- e ===> t; \
   1.110 -\      !!te c t. c isof t ==> P(<<te,e_const(c)>,t>); \
   1.111 -\      !!te x. x:te_dom(te) ==> P(<<te,e_var(x)>,te_app te x>); \
   1.112 +\      !!te c t. c isof t ==> P(((te,e_const(c)),t)); \
   1.113 +\      !!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x)); \
   1.114  \      !!te x e t1 t2. \
   1.115 -\        te + {x |=> t1} |- e ===> t2 ==> P(<<te,fn x => e>,t1->t2>); \
   1.116 +\        te + {x |=> t1} |- e ===> t2 ==> P(((te,fn x => e),t1->t2)); \
   1.117  \      !!te f x e t1 t2. \
   1.118  \        te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==> \
   1.119 -\        P(<<te,fix f(x) = e>,t1->t2>); \
   1.120 +\        P(((te,fix f(x) = e),t1->t2)); \
   1.121  \      !!te e1 e2 t1 t2. \
   1.122  \        [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> \
   1.123 -\        P(<<te,e1 @ e2>,t2>) \
   1.124 +\        P(((te,e1 @ e2),t2)) \
   1.125  \   |] ==> \
   1.126 -\   P(<<te,e>,t>)";
   1.127 +\   P(((te,e),t))";
   1.128  by (resolve_tac (prems RL [lfp_elim2]) 1);
   1.129  by (rtac elab_fun_mono 1);
   1.130  by (rewtac elab_fun_def);
   1.131 @@ -545,7 +545,7 @@
   1.132  
   1.133  (* First strong indtroduction (co-induction) rule for hasty_rel *)
   1.134  
   1.135 -val prems = goalw MT.thy [hasty_rel_def] "c isof t ==> <v_const(c),t> : hasty_rel";
   1.136 +val prems = goalw MT.thy [hasty_rel_def] "c isof t ==> (v_const(c),t) : hasty_rel";
   1.137  by (cut_facts_tac prems 1);
   1.138  by (rtac gfp_coind2 1);
   1.139  by (rewtac MT.hasty_fun_def);
   1.140 @@ -561,9 +561,9 @@
   1.141  \       ve_dom(ve) = te_dom(te); \
   1.142  \       ! ev1. \
   1.143  \         ev1:ve_dom(ve) --> \
   1.144 -\         <ve_app ve ev1,te_app te ev1> : {<v_clos(<|ev,e,ve|>),t>} Un hasty_rel \
   1.145 +\         (ve_app ve ev1,te_app te ev1) : {(v_clos(<|ev,e,ve|>),t)} Un hasty_rel \
   1.146  \   |] ==> \
   1.147 -\   <v_clos(<|ev,e,ve|>),t> : hasty_rel";
   1.148 +\   (v_clos(<|ev,e,ve|>),t) : hasty_rel";
   1.149  by (cut_facts_tac prems 1);
   1.150  by (rtac gfp_coind2 1);
   1.151  by (rewtac hasty_fun_def);
   1.152 @@ -575,14 +575,14 @@
   1.153  (* Elimination rule for hasty_rel *)
   1.154  
   1.155  val prems = goalw MT.thy [hasty_rel_def]
   1.156 -  " [| !! c t.c isof t ==> P(<v_const(c),t>); \
   1.157 +  " [| !! c t.c isof t ==> P((v_const(c),t)); \
   1.158  \      !! te ev e t ve. \
   1.159  \        [| te |- fn ev => e ===> t; \
   1.160  \           ve_dom(ve) = te_dom(te); \
   1.161 -\           !ev1.ev1:ve_dom(ve) --> <ve_app ve ev1,te_app te ev1> : hasty_rel \
   1.162 -\        |] ==> P(<v_clos(<|ev,e,ve|>),t>); \
   1.163 -\      <v,t> : hasty_rel \
   1.164 -\   |] ==> P(<v,t>)";
   1.165 +\           !ev1.ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel \
   1.166 +\        |] ==> P((v_clos(<|ev,e,ve|>),t)); \
   1.167 +\      (v,t) : hasty_rel \
   1.168 +\   |] ==> P((v,t))";
   1.169  by (cut_facts_tac prems 1);
   1.170  by (etac gfp_elim2 1);
   1.171  by (rtac mono_hasty_fun 1);
   1.172 @@ -595,12 +595,12 @@
   1.173  qed "hasty_rel_elim0";
   1.174  
   1.175  val prems = goal MT.thy 
   1.176 -  " [| <v,t> : hasty_rel; \
   1.177 +  " [| (v,t) : hasty_rel; \
   1.178  \      !! c t.c isof t ==> P (v_const c) t; \
   1.179  \      !! te ev e t ve. \
   1.180  \        [| te |- fn ev => e ===> t; \
   1.181  \           ve_dom(ve) = te_dom(te); \
   1.182 -\           !ev1.ev1:ve_dom(ve) --> <ve_app ve ev1,te_app te ev1> : hasty_rel \
   1.183 +\           !ev1.ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel \
   1.184  \        |] ==> P (v_clos <|ev,e,ve|>) t \
   1.185  \   |] ==> P v t";
   1.186  by (res_inst_tac [("P","P")] infsys_p2 1);