src/ZF/Coind/Map.ML
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 1461 6bcb44e4d6e5
child 2034 5079fdf938dd
permissions -rw-r--r--
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1075
diff changeset
     1
(*  Title:      ZF/Coind/Map.ML
915
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1075
diff changeset
     3
    Author:     Jacob Frost, Cambridge University Computer Laboratory
915
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     4
    Copyright   1995  University of Cambridge
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     5
*)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     6
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     7
open Map;
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     8
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     9
(* ############################################################ *)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    10
(* Lemmas                                                       *)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    11
(* ############################################################ *)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    12
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    13
goal Map.thy "!!A. a:A ==> Sigma(A,B)``{a} = B(a)";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    14
by (fast_tac eq_cs 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    15
qed "qbeta";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    16
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    17
goal Map.thy "!!A. a~:A ==> Sigma(A,B)``{a} = 0";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    18
by (fast_tac eq_cs 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    19
qed "qbeta_emp";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    20
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    21
goal Map.thy "!!A.a ~: A ==> Sigma(A,B)``{a}=0";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    22
by (fast_tac eq_cs 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    23
qed "image_Sigma1";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    24
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    25
goal Map.thy "0``A = 0";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    26
by (fast_tac eq_cs 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    27
qed "image_02";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    28
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    29
(* ############################################################ *)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    30
(* Inclusion in Quine Universes                                 *)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    31
(* ############################################################ *)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    32
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    33
(* Lemmas *)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    34
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    35
goalw Map.thy [quniv_def]
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    36
    "!!A. A <= univ(X) ==> Pow(A * Union(quniv(X))) <= quniv(X)";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    37
by (rtac Pow_mono 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    38
by (rtac ([Sigma_mono, product_univ] MRS subset_trans) 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    39
by (etac subset_trans 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    40
by (rtac (arg_subset_eclose RS univ_mono) 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    41
by (simp_tac (ZF_ss addsimps [Union_Pow_eq]) 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    42
qed "MapQU_lemma";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    43
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    44
(* Theorems *)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    45
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    46
val prems = goalw Map.thy [PMap_def,TMap_def]
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    47
  "[| m:PMap(A,quniv(B)); !!x.x:A ==> x:univ(B) |] ==> m:quniv(B)";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    48
by (cut_facts_tac prems 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    49
by (rtac (MapQU_lemma RS subsetD) 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    50
by (rtac subsetI 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    51
by (eresolve_tac prems 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    52
by (fast_tac ZF_cs 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    53
qed "mapQU";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    54
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    55
(* ############################################################ *)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    56
(* Monotonicity                                                 *)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    57
(* ############################################################ *)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    58
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    59
goalw Map.thy [PMap_def,TMap_def] "!!A.B<=C ==> PMap(A,B)<=PMap(A,C)";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    60
by (fast_tac ZF_cs 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    61
qed "map_mono";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    62
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    63
(* Rename to pmap_mono *)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    64
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    65
(* ############################################################ *)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    66
(* Introduction Rules                                           *)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    67
(* ############################################################ *)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    68
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    69
(** map_emp **)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    70
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    71
goalw Map.thy [map_emp_def,PMap_def,TMap_def] "map_emp:PMap(A,B)";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    72
by (safe_tac ZF_cs);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    73
by (rtac image_02 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    74
qed "pmap_empI";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    75
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    76
(** map_owr **)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    77
1020
76d72126a9e7 Modified proofs for new hyp_subst_tac, and simplified them.
lcp
parents: 915
diff changeset
    78
915
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    79
goalw Map.thy [map_owr_def,PMap_def,TMap_def] 
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    80
  "!! A.[| m:PMap(A,B); a:A; b:B |]  ==> map_owr(m,a,b):PMap(A,B)";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    81
by (safe_tac ZF_cs);
1075
848bf2e18dff Modified proofs for new claset primitives. The problem is that they enforce
lcp
parents: 1020
diff changeset
    82
by (ALLGOALS (asm_full_simp_tac (ZF_ss addsimps [if_iff])));
848bf2e18dff Modified proofs for new claset primitives. The problem is that they enforce
lcp
parents: 1020
diff changeset
    83
by (fast_tac ZF_cs 1);
915
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    84
by (fast_tac ZF_cs 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    85
by (fast_tac ZF_cs 1);
1075
848bf2e18dff Modified proofs for new claset primitives. The problem is that they enforce
lcp
parents: 1020
diff changeset
    86
915
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    87
by (rtac (excluded_middle RS disjE) 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    88
by (etac image_Sigma1 1);
1075
848bf2e18dff Modified proofs for new claset primitives. The problem is that they enforce
lcp
parents: 1020
diff changeset
    89
by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 1);
848bf2e18dff Modified proofs for new claset primitives. The problem is that they enforce
lcp
parents: 1020
diff changeset
    90
by (asm_full_simp_tac
848bf2e18dff Modified proofs for new claset primitives. The problem is that they enforce
lcp
parents: 1020
diff changeset
    91
 (ZF_ss addsimps [qbeta] setloop split_tac [expand_if]) 1);
1020
76d72126a9e7 Modified proofs for new hyp_subst_tac, and simplified them.
lcp
parents: 915
diff changeset
    92
by (safe_tac FOL_cs);
1075
848bf2e18dff Modified proofs for new claset primitives. The problem is that they enforce
lcp
parents: 1020
diff changeset
    93
by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 3);
848bf2e18dff Modified proofs for new claset primitives. The problem is that they enforce
lcp
parents: 1020
diff changeset
    94
by (ALLGOALS (asm_full_simp_tac ZF_ss));
915
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    95
by (fast_tac ZF_cs 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    96
qed "pmap_owrI";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    97
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    98
(** map_app **)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    99
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   100
goalw Map.thy [TMap_def,map_app_def] 
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   101
  "!!m.[| m:TMap(A,B); a:domain(m) |] ==> map_app(m,a) ~=0";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   102
by (etac domainE 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   103
by (dtac imageI 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   104
by (fast_tac ZF_cs 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   105
by (etac not_emptyI 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   106
qed "tmap_app_notempty";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   107
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   108
goalw Map.thy [TMap_def,map_app_def,domain_def] 
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   109
  "!!m.[| m:TMap(A,B); a:domain(m) |] ==> map_app(m,a):B";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   110
by (fast_tac eq_cs 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   111
qed "tmap_appI";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   112
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   113
goalw Map.thy [PMap_def]
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   114
  "!!m.[| m:PMap(A,B); a:domain(m) |] ==> map_app(m,a):B";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   115
by (forward_tac [tmap_app_notempty] 1); 
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   116
by (assume_tac 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   117
by (dtac tmap_appI 1); 
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   118
by (assume_tac 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   119
by (fast_tac ZF_cs 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   120
qed "pmap_appI";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   121
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   122
(** domain **)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   123
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   124
goalw Map.thy [TMap_def]
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   125
  "!!m.[| m:TMap(A,B); a:domain(m) |] ==> a:A";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   126
by (fast_tac eq_cs 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   127
qed "tmap_domainD";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   128
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   129
goalw Map.thy [PMap_def,TMap_def]
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   130
  "!!m.[| m:PMap(A,B); a:domain(m) |] ==> a:A";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   131
by (fast_tac eq_cs 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   132
qed "pmap_domainD";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   133
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   134
(* ############################################################ *)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   135
(* Equalitites                                                  *)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   136
(* ############################################################ *)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   137
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   138
(** Domain **)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   139
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   140
(* Lemmas *)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   141
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   142
goal Map.thy  "domain(UN x:A.B(x)) = (UN x:A.domain(B(x)))";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   143
by (fast_tac eq_cs 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   144
qed "domain_UN";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   145
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   146
goal Map.thy  "domain(Sigma(A,B)) = {x:A.EX y.y:B(x)}";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   147
by (simp_tac (ZF_ss addsimps [domain_UN,domain_0,domain_cons]) 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   148
by (fast_tac eq_cs 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   149
qed "domain_Sigma";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   150
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   151
(* Theorems *)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   152
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   153
goalw Map.thy [map_emp_def] "domain(map_emp) = 0";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   154
by (fast_tac eq_cs 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   155
qed "map_domain_emp";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   156
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   157
goalw Map.thy [map_owr_def] 
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   158
  "!!a.b ~= 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   159
by (simp_tac (if_ss addsimps [domain_Sigma]) 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   160
by (rtac equalityI 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   161
by (fast_tac eq_cs 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   162
by (rtac subsetI 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   163
by (rtac CollectI 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   164
by (assume_tac 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   165
by (etac UnE' 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   166
by (etac singletonE 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   167
by (asm_simp_tac if_ss 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   168
by (fast_tac eq_cs 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   169
by (etac notsingletonE 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   170
by (asm_simp_tac if_ss 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   171
by (fast_tac eq_cs 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   172
qed "map_domain_owr";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   173
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   174
(** Application **)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   175
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   176
goalw Map.thy [map_app_def,map_owr_def] 
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   177
  "map_app(map_owr(f,a,b),a) = b";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   178
by (rtac (qbeta RS ssubst) 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   179
by (fast_tac ZF_cs 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   180
by (simp_tac if_ss 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   181
qed "map_app_owr1";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   182
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   183
goalw Map.thy [map_app_def,map_owr_def] 
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   184
  "!!a.c ~= a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   185
by (rtac (excluded_middle RS disjE) 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   186
by (rtac (qbeta_emp RS ssubst) 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   187
by (assume_tac 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   188
by (fast_tac eq_cs 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   189
by (etac (qbeta RS ssubst) 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   190
by (asm_simp_tac if_ss 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   191
qed "map_app_owr2";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   192
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   193
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   194
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   195
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   196
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   197
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   198
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   199
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   200
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   201
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   202
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   203
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   204
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   205
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   206
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   207
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   208
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   209
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   210
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   211
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   212
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   213
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   214
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   215
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   216
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   217
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   218
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   219
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   220
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   221
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   222
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   223
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   224
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   225
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   226
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   227
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   228
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   229
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   230
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   231
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   232