src/HOLCF/ssum1.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 243 c22b85994e17
permissions -rw-r--r--
tidying
     1 (*  Title: 	HOLCF/ssum1.ML
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993  Technische Universitaet Muenchen
     5 
     6 Lemmas for theory ssum1.thy
     7 *)
     8 
     9 open Ssum1;
    10 
    11 local 
    12 
    13 fun eq_left s1 s2 = 
    14 	(
    15 	(res_inst_tac [("s",s1),("t",s2)] (inject_Isinl RS subst) 1)
    16 	THEN 	(rtac trans 1)
    17 	THEN 	(atac 2)
    18 	THEN 	(etac sym 1));
    19 
    20 fun eq_right s1 s2 = 
    21 	(
    22 	(res_inst_tac [("s",s1),("t",s2)] (inject_Isinr RS subst) 1)
    23 	THEN 	(rtac trans 1)
    24 	THEN 	(atac 2)
    25 	THEN 	(etac sym 1));
    26 
    27 fun UU_left s1 = 
    28 	(
    29 	(res_inst_tac [("t",s1)](noteq_IsinlIsinr RS conjunct1 RS ssubst)1)
    30 	THEN (rtac trans 1)
    31 	THEN (atac 2)
    32 	THEN (etac sym 1));
    33 
    34 fun UU_right s1 = 
    35 	(
    36 	(res_inst_tac [("t",s1)](noteq_IsinlIsinr RS conjunct2 RS ssubst)1)
    37 	THEN (rtac trans 1)
    38 	THEN (atac 2)
    39 	THEN (etac sym 1))
    40 
    41 in
    42 
    43 val less_ssum1a = prove_goalw Ssum1.thy [less_ssum_def]
    44 "[|s1=Isinl(x); s2=Isinl(y)|] ==> less_ssum(s1,s2) = (x << y)"
    45  (fn prems =>
    46 	[
    47 	(cut_facts_tac prems 1),
    48 	(rtac  select_equality 1),
    49 	(dtac conjunct1 2),
    50 	(dtac spec 2),
    51 	(dtac spec 2),
    52 	(etac mp 2),
    53 	(fast_tac HOL_cs 2),
    54 	(rtac conjI 1),
    55 	(strip_tac 1),
    56 	(etac conjE 1),
    57 	(eq_left "x" "u"),
    58 	(eq_left "y" "xa"),
    59 	(rtac refl 1),
    60 	(rtac conjI 1),
    61 	(strip_tac 1),
    62 	(etac conjE 1),
    63 	(UU_left "x"),
    64 	(UU_right "v"),
    65 	(simp_tac Cfun_ss 1),
    66 	(rtac conjI 1),
    67 	(strip_tac 1),
    68 	(etac conjE 1),
    69 	(eq_left "x" "u"),
    70 	(UU_left "y"),
    71 	(rtac iffI 1),
    72 	(etac UU_I 1),
    73 	(res_inst_tac [("s","x"),("t","UU")] subst 1),
    74 	(atac 1),
    75 	(rtac refl_less 1),
    76 	(strip_tac 1),
    77 	(etac conjE 1),
    78 	(UU_left "x"),
    79 	(UU_right "v"),
    80 	(simp_tac Cfun_ss 1)
    81 	]);
    82 
    83 
    84 val less_ssum1b = prove_goalw Ssum1.thy [less_ssum_def]
    85 "[|s1=Isinr(x); s2=Isinr(y)|] ==> less_ssum(s1,s2) = (x << y)"
    86  (fn prems =>
    87 	[
    88 	(cut_facts_tac prems 1),
    89 	(rtac  select_equality 1),
    90 	(dtac conjunct2 2),
    91 	(dtac conjunct1 2),
    92 	(dtac spec 2),
    93 	(dtac spec 2),
    94 	(etac mp 2),
    95 	(fast_tac HOL_cs 2),
    96 	(rtac conjI 1),
    97 	(strip_tac 1),
    98 	(etac conjE 1),
    99 	(UU_right "x"),
   100 	(UU_left "u"),
   101 	(simp_tac Cfun_ss 1),
   102 	(rtac conjI 1),
   103 	(strip_tac 1),
   104 	(etac conjE 1),
   105 	(eq_right "x" "v"),
   106 	(eq_right "y" "ya"),
   107 	(rtac refl 1),
   108 	(rtac conjI 1),
   109 	(strip_tac 1),
   110 	(etac conjE 1),
   111 	(UU_right "x"),
   112 	(UU_left "u"),
   113 	(simp_tac Cfun_ss 1),
   114 	(strip_tac 1),
   115 	(etac conjE 1),
   116 	(eq_right "x" "v"),
   117 	(UU_right "y"),
   118 	(rtac iffI 1),
   119 	(etac UU_I 1),
   120 	(res_inst_tac [("s","UU"),("t","x")] subst 1),
   121 	(etac sym 1),
   122 	(rtac refl_less 1)
   123 	]);
   124 
   125 
   126 val less_ssum1c = prove_goalw Ssum1.thy [less_ssum_def]
   127 "[|s1=Isinl(x); s2=Isinr(y)|] ==> less_ssum(s1,s2) = (x = UU)"
   128  (fn prems =>
   129 	[
   130 	(cut_facts_tac prems 1),
   131 	(rtac  select_equality 1),
   132 	(rtac conjI 1),
   133 	(strip_tac 1),
   134 	(etac conjE 1),
   135 	(eq_left  "x" "u"),
   136 	(UU_left "xa"),
   137 	(rtac iffI 1),
   138 	(res_inst_tac [("s","x"),("t","UU")] subst 1),
   139 	(atac 1),
   140 	(rtac refl_less 1),
   141 	(etac UU_I 1),
   142 	(rtac conjI 1),
   143 	(strip_tac 1),
   144 	(etac conjE 1),
   145 	(UU_left "x"),
   146 	(UU_right "v"),
   147 	(simp_tac Cfun_ss 1),
   148 	(rtac conjI 1),
   149 	(strip_tac 1),
   150 	(etac conjE 1),
   151 	(eq_left  "x" "u"),
   152 	(rtac refl 1),
   153 	(strip_tac 1),
   154 	(etac conjE 1),
   155 	(UU_left "x"),
   156 	(UU_right "v"),
   157 	(simp_tac Cfun_ss 1),
   158 	(dtac conjunct2 1),
   159 	(dtac conjunct2 1),
   160 	(dtac conjunct1 1),
   161 	(dtac spec 1),
   162 	(dtac spec 1),
   163 	(etac mp 1),
   164 	(fast_tac HOL_cs 1)
   165 	]);
   166 
   167 
   168 val less_ssum1d = prove_goalw Ssum1.thy [less_ssum_def]
   169 "[|s1=Isinr(x); s2=Isinl(y)|] ==> less_ssum(s1,s2) = (x = UU)"
   170  (fn prems =>
   171 	[
   172 	(cut_facts_tac prems 1),
   173 	(rtac  select_equality 1),
   174 	(dtac conjunct2 2),
   175 	(dtac conjunct2 2),
   176 	(dtac conjunct2 2),
   177 	(dtac spec 2),
   178 	(dtac spec 2),
   179 	(etac mp 2),
   180 	(fast_tac HOL_cs 2),
   181 	(rtac conjI 1),
   182 	(strip_tac 1),
   183 	(etac conjE 1),
   184 	(UU_right "x"),
   185 	(UU_left "u"),
   186 	(simp_tac Cfun_ss 1),
   187 	(rtac conjI 1),
   188 	(strip_tac 1),
   189 	(etac conjE 1),
   190 	(UU_right "ya"),
   191 	(eq_right "x" "v"),
   192 	(rtac iffI 1),
   193 	(etac UU_I 2),
   194 	(res_inst_tac [("s","UU"),("t","x")] subst 1),
   195 	(etac sym 1),
   196 	(rtac refl_less 1),
   197 	(rtac conjI 1),
   198 	(strip_tac 1),
   199 	(etac conjE 1),
   200 	(UU_right "x"),
   201 	(UU_left "u"),
   202 	(simp_tac HOL_ss 1),
   203 	(strip_tac 1),
   204 	(etac conjE 1),
   205 	(eq_right "x" "v"),
   206 	(rtac refl 1)
   207 	])
   208 end;
   209 
   210 
   211 (* ------------------------------------------------------------------------ *)
   212 (* optimize lemmas about less_ssum                                          *)
   213 (* ------------------------------------------------------------------------ *)
   214 
   215 val less_ssum2a = prove_goal Ssum1.thy 
   216 	"less_ssum(Isinl(x),Isinl(y)) = (x << y)"
   217  (fn prems =>
   218 	[
   219 	(rtac less_ssum1a 1),
   220 	(rtac refl 1),
   221 	(rtac refl 1)
   222 	]);
   223 
   224 val less_ssum2b = prove_goal Ssum1.thy 
   225 	"less_ssum(Isinr(x),Isinr(y)) = (x << y)"
   226  (fn prems =>
   227 	[
   228 	(rtac less_ssum1b 1),
   229 	(rtac refl 1),
   230 	(rtac refl 1)
   231 	]);
   232 
   233 val less_ssum2c = prove_goal Ssum1.thy 
   234 	"less_ssum(Isinl(x),Isinr(y)) = (x = UU)"
   235  (fn prems =>
   236 	[
   237 	(rtac less_ssum1c 1),
   238 	(rtac refl 1),
   239 	(rtac refl 1)
   240 	]);
   241 
   242 val less_ssum2d = prove_goal Ssum1.thy 
   243 	"less_ssum(Isinr(x),Isinl(y)) = (x = UU)"
   244  (fn prems =>
   245 	[
   246 	(rtac less_ssum1d 1),
   247 	(rtac refl 1),
   248 	(rtac refl 1)
   249 	]);
   250 
   251 
   252 (* ------------------------------------------------------------------------ *)
   253 (* less_ssum is a partial order on ++                                     *)
   254 (* ------------------------------------------------------------------------ *)
   255 
   256 val refl_less_ssum = prove_goal Ssum1.thy "less_ssum(p,p)"
   257  (fn prems =>
   258 	[
   259 	(res_inst_tac [("p","p")] IssumE2 1),
   260 	(hyp_subst_tac 1),
   261 	(rtac (less_ssum2a RS iffD2) 1),
   262 	(rtac refl_less 1),
   263 	(hyp_subst_tac 1),
   264 	(rtac (less_ssum2b RS iffD2) 1),
   265 	(rtac refl_less 1)
   266 	]);
   267 
   268 val antisym_less_ssum = prove_goal Ssum1.thy 
   269  "[|less_ssum(p1,p2);less_ssum(p2,p1)|] ==> p1=p2"
   270  (fn prems =>
   271 	[
   272 	(cut_facts_tac prems 1),
   273 	(res_inst_tac [("p","p1")] IssumE2 1),
   274 	(hyp_subst_tac 1),
   275 	(res_inst_tac [("p","p2")] IssumE2 1),
   276 	(hyp_subst_tac 1),
   277 	(res_inst_tac [("f","Isinl")] arg_cong 1),
   278 	(rtac antisym_less 1),
   279 	(etac (less_ssum2a RS iffD1) 1),
   280 	(etac (less_ssum2a RS iffD1) 1),
   281 	(hyp_subst_tac 1),
   282 	(etac (less_ssum2d RS iffD1 RS ssubst) 1),
   283 	(etac (less_ssum2c RS iffD1 RS ssubst) 1),
   284 	(rtac strict_IsinlIsinr 1),
   285 	(hyp_subst_tac 1),
   286 	(res_inst_tac [("p","p2")] IssumE2 1),
   287 	(hyp_subst_tac 1),
   288 	(etac (less_ssum2c RS iffD1 RS ssubst) 1),
   289 	(etac (less_ssum2d RS iffD1 RS ssubst) 1),
   290 	(rtac (strict_IsinlIsinr RS sym) 1),
   291 	(hyp_subst_tac 1),
   292 	(res_inst_tac [("f","Isinr")] arg_cong 1),
   293 	(rtac antisym_less 1),
   294 	(etac (less_ssum2b RS iffD1) 1),
   295 	(etac (less_ssum2b RS iffD1) 1)
   296 	]);
   297 
   298 val trans_less_ssum = prove_goal Ssum1.thy 
   299  "[|less_ssum(p1,p2);less_ssum(p2,p3)|] ==> less_ssum(p1,p3)"
   300  (fn prems =>
   301 	[
   302 	(cut_facts_tac prems 1),
   303 	(res_inst_tac [("p","p1")] IssumE2 1),
   304 	(hyp_subst_tac 1),
   305 	(res_inst_tac [("p","p3")] IssumE2 1),
   306 	(hyp_subst_tac 1),
   307 	(rtac (less_ssum2a RS iffD2) 1),
   308 	(res_inst_tac [("p","p2")] IssumE2 1),
   309 	(hyp_subst_tac 1),
   310 	(rtac trans_less 1),
   311 	(etac (less_ssum2a RS iffD1) 1),
   312 	(etac (less_ssum2a RS iffD1) 1),
   313 	(hyp_subst_tac 1),
   314 	(etac (less_ssum2c RS iffD1 RS ssubst) 1),
   315 	(rtac minimal 1),
   316 	(hyp_subst_tac 1),
   317 	(rtac (less_ssum2c RS iffD2) 1),
   318 	(res_inst_tac [("p","p2")] IssumE2 1),
   319 	(hyp_subst_tac 1),
   320 	(rtac UU_I 1),
   321 	(rtac trans_less 1),
   322 	(etac (less_ssum2a RS iffD1) 1),
   323 	(rtac (antisym_less_inverse RS conjunct1) 1),
   324 	(etac (less_ssum2c RS iffD1) 1),
   325 	(hyp_subst_tac 1),
   326 	(etac (less_ssum2c RS iffD1) 1),
   327 	(hyp_subst_tac 1),
   328 	(res_inst_tac [("p","p3")] IssumE2 1),
   329 	(hyp_subst_tac 1),
   330 	(rtac (less_ssum2d RS iffD2) 1),
   331 	(res_inst_tac [("p","p2")] IssumE2 1),
   332 	(hyp_subst_tac 1),
   333 	(etac (less_ssum2d RS iffD1) 1),
   334 	(hyp_subst_tac 1),
   335 	(rtac UU_I 1),
   336 	(rtac trans_less 1),
   337 	(etac (less_ssum2b RS iffD1) 1),
   338 	(rtac (antisym_less_inverse RS conjunct1) 1),
   339 	(etac (less_ssum2d RS iffD1) 1),
   340 	(hyp_subst_tac 1),
   341 	(rtac (less_ssum2b RS iffD2) 1),
   342 	(res_inst_tac [("p","p2")] IssumE2 1),
   343 	(hyp_subst_tac 1),
   344 	(etac (less_ssum2d RS iffD1 RS ssubst) 1),
   345 	(rtac minimal 1),
   346 	(hyp_subst_tac 1),
   347 	(rtac trans_less 1),
   348 	(etac (less_ssum2b RS iffD1) 1),
   349 	(etac (less_ssum2b RS iffD1) 1)
   350 	]);
   351 
   352 
   353