1 (* Title: HOL/BCV/Product.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 2000 TUM |
|
5 *) |
|
6 |
|
7 Goalw [lesub_def] "p <=(rA,rB) q == le rA rB p q"; |
|
8 by (Simp_tac 1); |
|
9 qed "unfold_lesub_prod"; |
|
10 |
|
11 Goalw [lesub_def,le_def] |
|
12 "((a1,b1) <=(rA,rB) (a2,b2)) = (a1 <=_rA a2 & b1 <=_rB b2)"; |
|
13 by (Simp_tac 1); |
|
14 qed "le_prod_Pair_conv"; |
|
15 AddIffs [le_prod_Pair_conv]; |
|
16 |
|
17 Goalw [lesssub_def] |
|
18 "((a1,b1) <_(Product.le rA rB) (a2,b2)) = \ |
|
19 \ (a1 <_rA a2 & b1 <=_rB b2 | a1 <=_rA a2 & b1 <_rB b2)"; |
|
20 by (Simp_tac 1); |
|
21 by (Blast_tac 1); |
|
22 qed "less_prod_Pair_conv"; |
|
23 |
|
24 Goalw [order_def] "order(Product.le rA rB) = (order rA & order rB)"; |
|
25 by (Simp_tac 1); |
|
26 by (Blast_tac 1); |
|
27 qed "order_le_prod"; |
|
28 AddIffs [order_le_prod]; |
|
29 |
|
30 |
|
31 Goalw [acc_def] "[| acc rA; acc rB |] ==> acc(Product.le rA rB)"; |
|
32 by (rtac wf_subset 1); |
|
33 by (etac wf_lex_prod 1); |
|
34 by (assume_tac 1); |
|
35 by (auto_tac (claset(), simpset() |
|
36 addsimps [lesssub_def,less_prod_Pair_conv,lex_prod_def])); |
|
37 qed "acc_le_prodI"; |
|
38 AddSIs [acc_le_prodI]; |
|
39 |
|
40 |
|
41 Goalw [closed_def,plussub_def,lift2_def,err_def,sup_def] |
|
42 "[| closed (err A) (lift2 f); closed (err B) (lift2 g) |] ==> \ |
|
43 \ closed (err(A<*>B)) (lift2(sup f g))"; |
|
44 by (asm_full_simp_tac (simpset() addsplits [err.split]) 1); |
|
45 by (Blast_tac 1); |
|
46 qed "closed_lift2_sup"; |
|
47 |
|
48 Goalw [plussub_def] "e1 +_(lift2 f) e2 == lift2 f e1 e2"; |
|
49 by (Simp_tac 1); |
|
50 qed "unfold_plussub_lift2"; |
|
51 |
|
52 Goal |
|
53 "[| x:A; y:A; semilat(err A, Err.le r, lift2 f) |] ==> \ |
|
54 \ (x +_f y = Err) = (~(? z:A. x <=_r z & y <=_r z))"; |
|
55 by (rtac iffI 1); |
|
56 by (Clarify_tac 1); |
|
57 by (dtac (OK_le_err_OK RS iffD2) 1); |
|
58 by (dtac (OK_le_err_OK RS iffD2) 1); |
|
59 by (dtac semilat_lub 1); |
|
60 by (assume_tac 1); |
|
61 by (assume_tac 1); |
|
62 by (Asm_simp_tac 1); |
|
63 by (Asm_simp_tac 1); |
|
64 by (Asm_simp_tac 1); |
|
65 by (Asm_full_simp_tac 1); |
|
66 by (case_tac "x +_f y" 1); |
|
67 by (assume_tac 1); |
|
68 by (rename_tac "z" 1); |
|
69 by (subgoal_tac "OK z: err A" 1); |
|
70 by (ftac (rotate_prems 2 (read_instantiate_sg(sign_of Err.thy)[("x","OK(x::'a)"),("y","OK(y::'a)")]plus_le_conv RS iffD1))1); |
|
71 by (assume_tac 1); |
|
72 by (Asm_simp_tac 1); |
|
73 by (blast_tac (claset() addDs [semilatDorderI,order_refl]) 1); |
|
74 by (Asm_simp_tac 1); |
|
75 by (Asm_simp_tac 1); |
|
76 by (Blast_tac 1); |
|
77 by (etac subst 1); |
|
78 by (rewrite_goals_tac [semilat_def,err_def,closed_def]); |
|
79 by (Asm_full_simp_tac 1); |
|
80 qed "plus_eq_Err_conv"; |
|
81 Addsimps [plus_eq_Err_conv]; |
|
82 |
|
83 Goalw [esl_def,Err.sl_def] |
|
84 "!!L1 L2. [| err_semilat L1; err_semilat L2 |] ==> err_semilat(Product.esl L1 L2)"; |
|
85 by (split_all_tac 1); |
|
86 by (Asm_full_simp_tac 1); |
|
87 by (simp_tac (HOL_basic_ss addsimps [semilat_Def]) 1); |
|
88 by (asm_simp_tac(HOL_basic_ss addsimps[semilatDclosedI,closed_lift2_sup])1); |
|
89 by (simp_tac (HOL_basic_ss addsimps |
|
90 [unfold_lesub_err,Err.le_def,unfold_plussub_lift2,sup_def]) 1); |
|
91 by (auto_tac (claset() addEs [semilat_le_err_OK1,semilat_le_err_OK2], |
|
92 simpset() addsimps [lift2_def] addsplits [err.split])); |
|
93 by (blast_tac (claset() addDs [semilatDorderI]) 1); |
|
94 by (blast_tac (claset() addDs [semilatDorderI]) 1); |
|
95 |
|
96 by (rtac (OK_le_err_OK RS iffD1) 1); |
|
97 by (etac subst 1 THEN stac (OK_lift2_OK RS sym) 1 THEN rtac semilat_lub 1); |
|
98 by (Asm_simp_tac 1); |
|
99 by (Asm_simp_tac 1); |
|
100 by (Asm_simp_tac 1); |
|
101 by (Asm_simp_tac 1); |
|
102 by (Asm_simp_tac 1); |
|
103 by (Asm_simp_tac 1); |
|
104 |
|
105 by (rtac (OK_le_err_OK RS iffD1) 1); |
|
106 by (etac subst 1 THEN stac (OK_lift2_OK RS sym) 1 THEN rtac semilat_lub 1); |
|
107 by (Asm_simp_tac 1); |
|
108 by (Asm_simp_tac 1); |
|
109 by (Asm_simp_tac 1); |
|
110 by (Asm_simp_tac 1); |
|
111 by (Asm_simp_tac 1); |
|
112 by (Asm_simp_tac 1); |
|
113 |
|
114 qed "err_semilat_Product_esl"; |
|