src/HOLCF/Up1.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 4098 71e05eb27fb6
child 6543 da7b170fc8a7
permissions -rw-r--r--
tidying
     1 (*  Title:      HOLCF/Up1.ML
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993  Technische Universitaet Muenchen
     5 *)
     6 
     7 open Up1;
     8 
     9 qed_goal "Abs_Up_inverse2" thy "Rep_Up (Abs_Up y) = y"
    10  (fn prems =>
    11         [
    12 	(simp_tac (simpset() addsimps [Up_def,Abs_Up_inverse]) 1)
    13 	]);
    14 
    15 qed_goalw "Exh_Up" thy [Iup_def ]
    16         "z = Abs_Up(Inl ()) | (? x. z = Iup x)"
    17  (fn prems =>
    18         [
    19         (rtac (Rep_Up_inverse RS subst) 1),
    20         (res_inst_tac [("s","Rep_Up z")] sumE 1),
    21         (rtac disjI1 1),
    22         (res_inst_tac [("f","Abs_Up")] arg_cong 1),
    23         (rtac (unit_eq RS subst) 1),
    24         (atac 1),
    25         (rtac disjI2 1),
    26         (rtac exI 1),
    27         (res_inst_tac [("f","Abs_Up")] arg_cong 1),
    28         (atac 1)
    29         ]);
    30 
    31 qed_goal "inj_Abs_Up" thy "inj(Abs_Up)"
    32  (fn prems =>
    33         [
    34         (rtac inj_inverseI 1),
    35         (rtac Abs_Up_inverse2 1)
    36         ]);
    37 
    38 qed_goal "inj_Rep_Up" thy "inj(Rep_Up)"
    39  (fn prems =>
    40         [
    41         (rtac inj_inverseI 1),
    42         (rtac Rep_Up_inverse 1)
    43         ]);
    44 
    45 qed_goalw "inject_Iup" thy [Iup_def] "Iup x=Iup y ==> x=y"
    46  (fn prems =>
    47         [
    48         (cut_facts_tac prems 1),
    49         (rtac (inj_Inr RS injD) 1),
    50         (rtac (inj_Abs_Up RS injD) 1),
    51         (atac 1)
    52         ]);
    53 
    54 qed_goalw "defined_Iup" thy [Iup_def] "Iup x~=Abs_Up(Inl ())"
    55  (fn prems =>
    56         [
    57         (rtac notI 1),
    58         (rtac notE 1),
    59         (rtac Inl_not_Inr 1),
    60         (rtac sym 1),
    61         (etac (inj_Abs_Up RS  injD) 1)
    62         ]);
    63 
    64 
    65 qed_goal "upE"  thy
    66         "[| p=Abs_Up(Inl ()) ==> Q; !!x. p=Iup(x)==>Q|] ==>Q"
    67  (fn prems =>
    68         [
    69         (rtac (Exh_Up RS disjE) 1),
    70         (eresolve_tac prems 1),
    71         (etac exE 1),
    72         (eresolve_tac prems 1)
    73         ]);
    74 
    75 qed_goalw "Ifup1"  thy [Ifup_def]
    76         "Ifup(f)(Abs_Up(Inl ()))=UU"
    77  (fn prems =>
    78         [
    79         (stac Abs_Up_inverse2 1),
    80         (stac sum_case_Inl 1),
    81         (rtac refl 1)
    82         ]);
    83 
    84 qed_goalw "Ifup2"  thy [Ifup_def,Iup_def]
    85         "Ifup(f)(Iup(x))=f`x"
    86  (fn prems =>
    87         [
    88         (stac Abs_Up_inverse2 1),
    89         (stac sum_case_Inr 1),
    90         (rtac refl 1)
    91         ]);
    92 
    93 val Up0_ss = (simpset_of Cfun3.thy) addsimps [Ifup1,Ifup2];
    94 
    95 qed_goalw "less_up1a"  thy [less_up_def]
    96         "Abs_Up(Inl ())<< z"
    97  (fn prems =>
    98         [
    99         (stac Abs_Up_inverse2 1),
   100         (stac sum_case_Inl 1),
   101         (rtac TrueI 1)
   102         ]);
   103 
   104 qed_goalw "less_up1b" thy [Iup_def,less_up_def]
   105         "~(Iup x) << (Abs_Up(Inl ()))"
   106  (fn prems =>
   107         [
   108         (rtac notI 1),
   109         (rtac iffD1 1),
   110         (atac 2),
   111         (stac Abs_Up_inverse2 1),
   112         (stac Abs_Up_inverse2 1),
   113         (stac sum_case_Inr 1),
   114         (stac sum_case_Inl 1),
   115         (rtac refl 1)
   116         ]);
   117 
   118 qed_goalw "less_up1c"  thy [Iup_def,less_up_def]
   119         " (Iup x) << (Iup y)=(x<<y)"
   120  (fn prems =>
   121         [
   122         (stac Abs_Up_inverse2 1),
   123         (stac Abs_Up_inverse2 1),
   124         (stac sum_case_Inr 1),
   125         (stac sum_case_Inr 1),
   126         (rtac refl 1)
   127         ]);
   128 
   129 
   130 qed_goal "refl_less_up"  thy "(p::'a u) << p"
   131  (fn prems =>
   132         [
   133         (res_inst_tac [("p","p")] upE 1),
   134         (hyp_subst_tac 1),
   135         (rtac less_up1a 1),
   136         (hyp_subst_tac 1),
   137         (rtac (less_up1c RS iffD2) 1),
   138         (rtac refl_less 1)
   139         ]);
   140 
   141 qed_goal "antisym_less_up"  thy 
   142         "!!p1.[|(p1::'a u) << p2;p2 << p1|] ==> p1=p2"
   143  (fn _ =>
   144         [
   145         (res_inst_tac [("p","p1")] upE 1),
   146         (hyp_subst_tac 1),
   147         (res_inst_tac [("p","p2")] upE 1),
   148         (etac sym 1),
   149         (hyp_subst_tac 1),
   150         (res_inst_tac [("P","(Iup x) << (Abs_Up(Inl ()))")] notE 1),
   151         (rtac less_up1b 1),
   152         (atac 1),
   153         (hyp_subst_tac 1),
   154         (res_inst_tac [("p","p2")] upE 1),
   155         (hyp_subst_tac 1),
   156         (res_inst_tac [("P","(Iup x) << (Abs_Up(Inl ()))")] notE 1),
   157         (rtac less_up1b 1),
   158         (atac 1),
   159         (hyp_subst_tac 1),
   160         (rtac arg_cong 1),
   161         (rtac antisym_less 1),
   162         (etac (less_up1c RS iffD1) 1),
   163         (etac (less_up1c RS iffD1) 1)
   164         ]);
   165 
   166 qed_goal "trans_less_up"  thy 
   167         "[|(p1::'a u) << p2;p2 << p3|] ==> p1 << p3"
   168  (fn prems =>
   169         [
   170         (cut_facts_tac prems 1),
   171         (res_inst_tac [("p","p1")] upE 1),
   172         (hyp_subst_tac 1),
   173         (rtac less_up1a 1),
   174         (hyp_subst_tac 1),
   175         (res_inst_tac [("p","p2")] upE 1),
   176         (hyp_subst_tac 1),
   177         (rtac notE 1),
   178         (rtac less_up1b 1),
   179         (atac 1),
   180         (hyp_subst_tac 1),
   181         (res_inst_tac [("p","p3")] upE 1),
   182         (hyp_subst_tac 1),
   183         (rtac notE 1),
   184         (rtac less_up1b 1),
   185         (atac 1),
   186         (hyp_subst_tac 1),
   187         (rtac (less_up1c RS iffD2) 1),
   188         (rtac trans_less 1),
   189         (etac (less_up1c RS iffD1) 1),
   190         (etac (less_up1c RS iffD1) 1)
   191         ]);
   192