src/HOL/Prod.ML
author paulson
Fri, 18 Feb 2000 15:35:29 +0100
changeset 8255 38f96394c099
parent 8157 b1a458416c92
child 8261 e4726ac0863a
permissions -rw-r--r--
new distributive laws
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1454
diff changeset
     1
(*  Title:      HOL/prod
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1454
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     5
5810
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
     6
Ordered Pairs, the Cartesian product type, the unit type
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     7
*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     8
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     9
(*This counts as a non-emptiness result for admitting 'a * 'b as a type*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4989
diff changeset
    10
Goalw [Prod_def] "Pair_Rep a b : Prod";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    11
by (EVERY1 [rtac CollectI, rtac exI, rtac exI, rtac refl]);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    12
qed "ProdI";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    13
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    14
val [major] = goalw Prod.thy [Pair_Rep_def]
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    15
    "Pair_Rep a b = Pair_Rep a' b' ==> a=a' & b=b'";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    16
by (EVERY1 [rtac (major RS fun_cong RS fun_cong RS subst), 
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1454
diff changeset
    17
            rtac conjI, rtac refl, rtac refl]);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    18
qed "Pair_Rep_inject";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    19
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4989
diff changeset
    20
Goal "inj_on Abs_Prod Prod";
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4828
diff changeset
    21
by (rtac inj_on_inverseI 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    22
by (etac Abs_Prod_inverse 1);
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4828
diff changeset
    23
qed "inj_on_Abs_Prod";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    24
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5303
diff changeset
    25
val prems = Goalw [Pair_def]
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 923
diff changeset
    26
    "[| (a, b) = (a',b');  [| a=a';  b=b' |] ==> R |] ==> R";
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4828
diff changeset
    27
by (rtac (inj_on_Abs_Prod RS inj_onD RS Pair_Rep_inject RS conjE) 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    28
by (REPEAT (ares_tac (prems@[ProdI]) 1));
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    29
qed "Pair_inject";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    30
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4989
diff changeset
    31
Goal "((a,b) = (a',b')) = (a=a' & b=b')";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
    32
by (blast_tac (claset() addSEs [Pair_inject]) 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    33
qed "Pair_eq";
3429
nipkow
parents: 2935
diff changeset
    34
AddIffs [Pair_eq];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    35
7495
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
    36
Goalw [fst_def] "fst (a,b) = a";
4534
6932c3ae3912 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
    37
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    38
qed "fst_conv";
7495
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
    39
Goalw [snd_def] "snd (a,b) = b";
4534
6932c3ae3912 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
    40
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    41
qed "snd_conv";
4534
6932c3ae3912 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
    42
Addsimps [fst_conv, snd_conv];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    43
7495
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
    44
Goal "fst (x, y) = a ==> x = a";
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
    45
by (Asm_full_simp_tac 1);
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
    46
qed "fst_eqD";
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
    47
Goal "snd (x, y) = a ==> y = a";
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
    48
by (Asm_full_simp_tac 1);
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
    49
qed "snd_eqD";
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
    50
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4989
diff changeset
    51
Goalw [Pair_def] "? x y. p = (x,y)";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    52
by (rtac (rewrite_rule [Prod_def] Rep_Prod RS CollectE) 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    53
by (EVERY1[etac exE, etac exE, rtac exI, rtac exI,
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1454
diff changeset
    54
           rtac (Rep_Prod_inverse RS sym RS trans),  etac arg_cong]);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    55
qed "PairE_lemma";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    56
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5303
diff changeset
    57
val [prem] = Goal "[| !!x y. p = (x,y) ==> Q |] ==> Q";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    58
by (rtac (PairE_lemma RS exE) 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    59
by (REPEAT (eresolve_tac [prem,exE] 1));
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    60
qed "PairE";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    61
4819
ef2e8e2a10e1 improved pair_tac to call prune_params_tac afterwards
oheimb
parents: 4799
diff changeset
    62
fun pair_tac s = EVERY' [res_inst_tac [("p",s)] PairE, hyp_subst_tac,
ef2e8e2a10e1 improved pair_tac to call prune_params_tac afterwards
oheimb
parents: 4799
diff changeset
    63
			 K prune_params_tac];
4134
5c6cb2a25816 added several theorems
oheimb
parents: 4089
diff changeset
    64
4828
ee3317896a47 improved split_all_tac significantly
oheimb
parents: 4819
diff changeset
    65
(* Do not add as rewrite rule: invalidates some proofs in IMP *)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4989
diff changeset
    66
Goal "p = (fst(p),snd(p))";
4828
ee3317896a47 improved split_all_tac significantly
oheimb
parents: 4819
diff changeset
    67
by (pair_tac "p" 1);
ee3317896a47 improved split_all_tac significantly
oheimb
parents: 4819
diff changeset
    68
by (Asm_simp_tac 1);
ee3317896a47 improved split_all_tac significantly
oheimb
parents: 4819
diff changeset
    69
qed "surjective_pairing";
ee3317896a47 improved split_all_tac significantly
oheimb
parents: 4819
diff changeset
    70
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
    71
Goal "? x y. z = (x, y)";
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
    72
by (rtac exI 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
    73
by (rtac exI 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
    74
by (rtac surjective_pairing 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
    75
qed "surj_pair";
4828
ee3317896a47 improved split_all_tac significantly
oheimb
parents: 4819
diff changeset
    76
Addsimps [surj_pair];
ee3317896a47 improved split_all_tac significantly
oheimb
parents: 4819
diff changeset
    77
ee3317896a47 improved split_all_tac significantly
oheimb
parents: 4819
diff changeset
    78
5699
5b9a359e083c split_paired_all.ML;
wenzelm
parents: 5553
diff changeset
    79
bind_thm ("split_paired_all",
5b9a359e083c split_paired_all.ML;
wenzelm
parents: 5553
diff changeset
    80
  SplitPairedAll.rule (standard (surjective_pairing RS eq_reflection)));
4828
ee3317896a47 improved split_all_tac significantly
oheimb
parents: 4819
diff changeset
    81
(*
ee3317896a47 improved split_all_tac significantly
oheimb
parents: 4819
diff changeset
    82
Addsimps [split_paired_all] does not work with simplifier 
ee3317896a47 improved split_all_tac significantly
oheimb
parents: 4819
diff changeset
    83
because it also affects premises in congrence rules, 
ee3317896a47 improved split_all_tac significantly
oheimb
parents: 4819
diff changeset
    84
where is can lead to premises of the form !!a b. ... = ?P(a,b)
ee3317896a47 improved split_all_tac significantly
oheimb
parents: 4819
diff changeset
    85
which cannot be solved by reflexivity.
ee3317896a47 improved split_all_tac significantly
oheimb
parents: 4819
diff changeset
    86
*)
ee3317896a47 improved split_all_tac significantly
oheimb
parents: 4819
diff changeset
    87
1301
42782316d510 Added various thms and tactics.
nipkow
parents: 1264
diff changeset
    88
(* replace parameters of product type by individual component parameters *)
42782316d510 Added various thms and tactics.
nipkow
parents: 1264
diff changeset
    89
local
4819
ef2e8e2a10e1 improved pair_tac to call prune_params_tac afterwards
oheimb
parents: 4799
diff changeset
    90
  fun is_pair (_,Type("*",_)) = true
ef2e8e2a10e1 improved pair_tac to call prune_params_tac afterwards
oheimb
parents: 4799
diff changeset
    91
    | is_pair  _              = false;
4828
ee3317896a47 improved split_all_tac significantly
oheimb
parents: 4819
diff changeset
    92
  fun exists_paired_all prem  = exists is_pair (Logic.strip_params prem);
ee3317896a47 improved split_all_tac significantly
oheimb
parents: 4819
diff changeset
    93
  val split_tac = full_simp_tac (HOL_basic_ss addsimps [split_paired_all]);
1301
42782316d510 Added various thms and tactics.
nipkow
parents: 1264
diff changeset
    94
in
4828
ee3317896a47 improved split_all_tac significantly
oheimb
parents: 4819
diff changeset
    95
val split_all_tac = SUBGOAL (fn (prem,i) => 
ee3317896a47 improved split_all_tac significantly
oheimb
parents: 4819
diff changeset
    96
    if exists_paired_all prem then split_tac i else no_tac);  
1301
42782316d510 Added various thms and tactics.
nipkow
parents: 1264
diff changeset
    97
end;
42782316d510 Added various thms and tactics.
nipkow
parents: 1264
diff changeset
    98
4828
ee3317896a47 improved split_all_tac significantly
oheimb
parents: 4819
diff changeset
    99
claset_ref() := claset() addSWrapper ("split_all_tac", 
ee3317896a47 improved split_all_tac significantly
oheimb
parents: 4819
diff changeset
   100
				      fn tac2 => split_all_tac ORELSE' tac2);
3568
36ff1ab12021 Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents: 3429
diff changeset
   101
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4989
diff changeset
   102
Goal "(!x. P x) = (!a b. P(a,b))";
4650
91af1ef45d68 added split_all_tac to claset()
oheimb
parents: 4534
diff changeset
   103
by (Fast_tac 1);
1301
42782316d510 Added various thms and tactics.
nipkow
parents: 1264
diff changeset
   104
qed "split_paired_All";
3568
36ff1ab12021 Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents: 3429
diff changeset
   105
Addsimps [split_paired_All];
36ff1ab12021 Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents: 3429
diff changeset
   106
(* AddIffs is not a good idea because it makes Blast_tac loop *)
36ff1ab12021 Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents: 3429
diff changeset
   107
5715
5fc697ad232b Added theorem prod_induct (needed for rep_datatype).
berghofe
parents: 5699
diff changeset
   108
bind_thm ("prod_induct",
5fc697ad232b Added theorem prod_induct (needed for rep_datatype).
berghofe
parents: 5699
diff changeset
   109
  allI RS (allI RS (split_paired_All RS iffD2)) RS spec);
5fc697ad232b Added theorem prod_induct (needed for rep_datatype).
berghofe
parents: 5699
diff changeset
   110
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4989
diff changeset
   111
Goal "(? x. P x) = (? a b. P(a,b))";
4650
91af1ef45d68 added split_all_tac to claset()
oheimb
parents: 4534
diff changeset
   112
by (Fast_tac 1);
3568
36ff1ab12021 Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents: 3429
diff changeset
   113
qed "split_paired_Ex";
4534
6932c3ae3912 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
   114
Addsimps [split_paired_Ex];
1301
42782316d510 Added various thms and tactics.
nipkow
parents: 1264
diff changeset
   115
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4989
diff changeset
   116
Goalw [split_def] "split c (a,b) = c a b";
4534
6932c3ae3912 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
   117
by (Simp_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   118
qed "split";
4534
6932c3ae3912 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
   119
Addsimps [split];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   120
7339
1b4d7a851b34 split_paired_Eps and lemmas
paulson
parents: 7031
diff changeset
   121
(*Subsumes the old split_Pair when f is the identity function*)
1b4d7a851b34 split_paired_Eps and lemmas
paulson
parents: 7031
diff changeset
   122
Goal "split (%x y. f(x,y)) = f";
1b4d7a851b34 split_paired_Eps and lemmas
paulson
parents: 7031
diff changeset
   123
by (rtac ext 1);
1b4d7a851b34 split_paired_Eps and lemmas
paulson
parents: 7031
diff changeset
   124
by (pair_tac "x" 1);
4828
ee3317896a47 improved split_all_tac significantly
oheimb
parents: 4819
diff changeset
   125
by (Simp_tac 1);
7339
1b4d7a851b34 split_paired_Eps and lemmas
paulson
parents: 7031
diff changeset
   126
qed "split_Pair_apply";
1b4d7a851b34 split_paired_Eps and lemmas
paulson
parents: 7031
diff changeset
   127
1b4d7a851b34 split_paired_Eps and lemmas
paulson
parents: 7031
diff changeset
   128
(*Can't be added to simpset: loops!*)
1b4d7a851b34 split_paired_Eps and lemmas
paulson
parents: 7031
diff changeset
   129
Goal "(SOME x. P x) = (SOME (a,b). P(a,b))";
1b4d7a851b34 split_paired_Eps and lemmas
paulson
parents: 7031
diff changeset
   130
by (simp_tac (simpset() addsimps [split_Pair_apply]) 1);
1b4d7a851b34 split_paired_Eps and lemmas
paulson
parents: 7031
diff changeset
   131
qed "split_paired_Eps";
4828
ee3317896a47 improved split_all_tac significantly
oheimb
parents: 4819
diff changeset
   132
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4989
diff changeset
   133
Goal "!!s t. (s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
4828
ee3317896a47 improved split_all_tac significantly
oheimb
parents: 4819
diff changeset
   134
by (split_all_tac 1);
1264
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 972
diff changeset
   135
by (Asm_simp_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   136
qed "Pair_fst_snd_eq";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   137
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   138
(*Prevents simplification of c: much faster*)
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   139
val [prem] = goal Prod.thy
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   140
  "p=q ==> split c p = split c q";
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   141
by (rtac (prem RS arg_cong) 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   142
qed "split_weak_cong";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   143
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   144
Goal "(%(x,y). f(x,y)) = f";
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   145
by (rtac ext 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   146
by (split_all_tac 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   147
by (rtac split 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   148
qed "split_eta";
1655
5be64540f275 Added a number of lemmas
nipkow
parents: 1642
diff changeset
   149
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   150
val prems = Goal "(!!x y. f x y = g(x,y)) ==> (%(x,y). f x y) = g";
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   151
by (asm_simp_tac (simpset() addsimps prems@[split_eta]) 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   152
qed "cond_split_eta";
5294
a84dd70e9925 replaced split_etas by split_eta_proc
oheimb
parents: 5278
diff changeset
   153
a84dd70e9925 replaced split_etas by split_eta_proc
oheimb
parents: 5278
diff changeset
   154
(*simplification procedure for cond_split_eta. 
a84dd70e9925 replaced split_etas by split_eta_proc
oheimb
parents: 5278
diff changeset
   155
  using split_eta a rewrite rule is not general enough, and using 
7495
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   156
  cond_split_eta directly would render some existing proofs very inefficient.
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   157
  similarly for split_beta. *)
5294
a84dd70e9925 replaced split_etas by split_eta_proc
oheimb
parents: 5278
diff changeset
   158
local
7495
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   159
  fun  Pair_pat k 0 (Bound m) = (m = k)
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   160
  |    Pair_pat k i (Const ("Pair",  _) $ Bound m $ t) = i > 0 andalso
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   161
			m = k+i andalso Pair_pat k (i-1) t
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   162
  |    Pair_pat _ _ _ = false;
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   163
  fun no_args k i (Abs (_, _, t)) = no_args (k+1) i t
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   164
  |   no_args k i (t $ u) = no_args k i t andalso no_args k i u
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   165
  |   no_args k i (Bound m) = m < k orelse m > k+i
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   166
  |   no_args _ _ _ = true;
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   167
  fun split_pat tp i (Abs  (_,_,t)) = if tp 0 i t then Some (i,t) else None
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   168
  |   split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   169
  |   split_pat tp i _ = None;
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   170
  fun metaeq sg lhs rhs = mk_meta_eq (prove_goalw_cterm [] 
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   171
	(cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs))))
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   172
	(K [simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1]));
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   173
  fun simproc name patstr = Simplifier.mk_simproc name 
8100
6186ee807f2e replaced HOLogic.termTVar by HOLogic.termT;
wenzelm
parents: 7958
diff changeset
   174
		[Thm.read_cterm (sign_of Prod.thy) (patstr, HOLogic.termT)];
7495
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   175
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   176
  val beta_patstr = "split f z";
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   177
  val  eta_patstr = "split f";
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   178
  fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   179
  |   beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   180
			(beta_term_pat k i t andalso beta_term_pat k i u)
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   181
  |   beta_term_pat k i t = no_args k i t;
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   182
  fun  eta_term_pat k i (f $ arg) = no_args k i f andalso Pair_pat k i arg
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   183
  |    eta_term_pat _ _ _ = false;
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   184
  fun subst arg k i (Abs (x, T, t)) = Abs (x, T, subst arg (k+1) i t)
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   185
  |   subst arg k i (t $ u) = if Pair_pat k i (t $ u) then incr_boundvars k arg
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   186
			      else (subst arg k i t $ subst arg k i u)
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   187
  |   subst arg k i t = t;
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   188
  fun beta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t) $ arg) = 
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   189
	(case split_pat beta_term_pat 1 t of 
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   190
	Some (i,f) => Some (metaeq sg s (subst arg 0 i f))
5294
a84dd70e9925 replaced split_etas by split_eta_proc
oheimb
parents: 5278
diff changeset
   191
	| None => None)
7495
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   192
  |   beta_proc _ _ _ = None;
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   193
  fun eta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t)) = 
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   194
	(case split_pat eta_term_pat 1 t of
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   195
	  Some (_,ft) => Some (metaeq sg s (let val (f $ arg) = ft in f end))
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   196
 	| None => None)
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   197
  |   eta_proc _ _ _ = None;
5294
a84dd70e9925 replaced split_etas by split_eta_proc
oheimb
parents: 5278
diff changeset
   198
in
7495
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   199
  val split_beta_proc = simproc "split_beta" beta_patstr beta_proc;
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   200
  val split_eta_proc  = simproc "split_eta"   eta_patstr  eta_proc;
5294
a84dd70e9925 replaced split_etas by split_eta_proc
oheimb
parents: 5278
diff changeset
   201
end;
a84dd70e9925 replaced split_etas by split_eta_proc
oheimb
parents: 5278
diff changeset
   202
7495
affcfd2830b7 added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents: 7339
diff changeset
   203
Addsimprocs [split_beta_proc,split_eta_proc];
5294
a84dd70e9925 replaced split_etas by split_eta_proc
oheimb
parents: 5278
diff changeset
   204
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   205
Goal "(%(x,y). P x y) z = P (fst z) (snd z)";
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   206
by (stac surjective_pairing 1 THEN rtac split 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   207
qed "split_beta";
4134
5c6cb2a25816 added several theorems
oheimb
parents: 4089
diff changeset
   208
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   209
(*For use with split_tac and the simplifier*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4989
diff changeset
   210
Goal "R (split c p) = (! x y. p = (x,y) --> R (c x y))";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   211
by (stac surjective_pairing 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   212
by (stac split 1);
2935
998cb95fdd43 Yet more fast_tac->blast_tac, and other tidying
paulson
parents: 2886
diff changeset
   213
by (Blast_tac 1);
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4828
diff changeset
   214
qed "split_split";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   215
3568
36ff1ab12021 Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents: 3429
diff changeset
   216
(* could be done after split_tac has been speeded up significantly:
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4828
diff changeset
   217
simpset_ref() := simpset() addsplits [split_split];
3568
36ff1ab12021 Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents: 3429
diff changeset
   218
   precompute the constants involved and don't do anything unless
36ff1ab12021 Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents: 3429
diff changeset
   219
   the current goal contains one of those constants
36ff1ab12021 Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents: 3429
diff changeset
   220
*)
36ff1ab12021 Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents: 3429
diff changeset
   221
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4989
diff changeset
   222
Goal "R (split c p) = (~(? x y. p = (x,y) & (~R (c x y))))";
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4828
diff changeset
   223
by (stac split_split 1);
4435
41a7e4f0e957 added expand_split_asm
oheimb
parents: 4423
diff changeset
   224
by (Simp_tac 1);
41a7e4f0e957 added expand_split_asm
oheimb
parents: 4423
diff changeset
   225
qed "expand_split_asm";
41a7e4f0e957 added expand_split_asm
oheimb
parents: 4423
diff changeset
   226
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   227
(** split used as a logical connective or set former **)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   228
2935
998cb95fdd43 Yet more fast_tac->blast_tac, and other tidying
paulson
parents: 2886
diff changeset
   229
(*These rules are for use with blast_tac.
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   230
  Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   231
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4989
diff changeset
   232
Goal "!!p. [| !!a b. p=(a,b) ==> c a b |] ==> split c p";
1552
6f71b5d46700 Ran expandshort
paulson
parents: 1515
diff changeset
   233
by (split_all_tac 1);
1454
d0266c81a85e Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents: 1301
diff changeset
   234
by (Asm_simp_tac 1);
d0266c81a85e Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents: 1301
diff changeset
   235
qed "splitI2";
d0266c81a85e Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents: 1301
diff changeset
   236
7958
f531589c9fc1 added various little lemmas
oheimb
parents: 7495
diff changeset
   237
Goal "!!p. [| !!a b. (a,b)=p ==> c a b x |] ==> split c p x";
f531589c9fc1 added various little lemmas
oheimb
parents: 7495
diff changeset
   238
by (split_all_tac 1);
f531589c9fc1 added various little lemmas
oheimb
parents: 7495
diff changeset
   239
by (Asm_simp_tac 1);
f531589c9fc1 added various little lemmas
oheimb
parents: 7495
diff changeset
   240
qed "splitI2'";
f531589c9fc1 added various little lemmas
oheimb
parents: 7495
diff changeset
   241
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5132
diff changeset
   242
Goal "c a b ==> split c (a,b)";
1264
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 972
diff changeset
   243
by (Asm_simp_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   244
qed "splitI";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   245
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5303
diff changeset
   246
val prems = Goalw [split_def]
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 923
diff changeset
   247
    "[| split c p;  !!x y. [| p = (x,y);  c x y |] ==> Q |] ==> Q";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   248
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   249
qed "splitE";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   250
8157
b1a458416c92 added splitE', also to claset
oheimb
parents: 8100
diff changeset
   251
val prems = Goalw [split_def]
b1a458416c92 added splitE', also to claset
oheimb
parents: 8100
diff changeset
   252
    "[| split c p z;  !!x y. [| p = (x,y);  c x y z |] ==> Q |] ==> Q";
b1a458416c92 added splitE', also to claset
oheimb
parents: 8100
diff changeset
   253
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
b1a458416c92 added splitE', also to claset
oheimb
parents: 8100
diff changeset
   254
qed "splitE'";
b1a458416c92 added splitE', also to claset
oheimb
parents: 8100
diff changeset
   255
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   256
val major::prems = goal Prod.thy 
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   257
    "[| Q (split P z);  !!x y. [|z = (x, y); Q (P x y)|] ==> R  \
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   258
\    |] ==> R";
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   259
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   260
by (rtac (split_beta RS subst) 1 THEN rtac major 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   261
qed "splitE2";
4134
5c6cb2a25816 added several theorems
oheimb
parents: 4089
diff changeset
   262
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5132
diff changeset
   263
Goal "split R (a,b) ==> R a b";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   264
by (etac (split RS iffD1) 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   265
qed "splitD";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   266
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5132
diff changeset
   267
Goal "z: c a b ==> z: split c (a,b)";
1264
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 972
diff changeset
   268
by (Asm_simp_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   269
qed "mem_splitI";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   270
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4989
diff changeset
   271
Goal "!!p. [| !!a b. p=(a,b) ==> z: c a b |] ==> z: split c p";
1552
6f71b5d46700 Ran expandshort
paulson
parents: 1515
diff changeset
   272
by (split_all_tac 1);
1454
d0266c81a85e Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents: 1301
diff changeset
   273
by (Asm_simp_tac 1);
d0266c81a85e Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents: 1301
diff changeset
   274
qed "mem_splitI2";
d0266c81a85e Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents: 1301
diff changeset
   275
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5303
diff changeset
   276
val prems = Goalw [split_def]
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 923
diff changeset
   277
    "[| z: split c p;  !!x y. [| p = (x,y);  z: c x y |] ==> Q |] ==> Q";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   278
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   279
qed "mem_splitE";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   280
7958
f531589c9fc1 added various little lemmas
oheimb
parents: 7495
diff changeset
   281
AddSIs [splitI, splitI2, splitI2', mem_splitI, mem_splitI2];
8157
b1a458416c92 added splitE', also to claset
oheimb
parents: 8100
diff changeset
   282
AddSEs [splitE, splitE', mem_splitE];
2856
cdb908486a96 Reorganization of how classical rules are installed
paulson
parents: 2637
diff changeset
   283
4534
6932c3ae3912 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
   284
(* allows simplifications of nested splits in case of independent predicates *)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4989
diff changeset
   285
Goal "(%(a,b). P & Q a b) = (%ab. P & split Q ab)";
4534
6932c3ae3912 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
   286
by (rtac ext 1);
6932c3ae3912 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
   287
by (Blast_tac 1);
6932c3ae3912 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
   288
qed "split_part";
6932c3ae3912 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
   289
Addsimps [split_part];
6932c3ae3912 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
   290
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4989
diff changeset
   291
Goal "(@(x',y'). x = x' & y = y') = (x,y)";
4534
6932c3ae3912 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
   292
by (Blast_tac 1);
6932c3ae3912 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
   293
qed "Eps_split_eq";
6932c3ae3912 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
   294
Addsimps [Eps_split_eq];
6932c3ae3912 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
   295
(*
6932c3ae3912 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
   296
the following  would be slightly more general, 
6932c3ae3912 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
   297
but cannot be used as rewrite rule:
6932c3ae3912 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
   298
### Cannot add premise as rewrite rule because it contains (type) unknowns:
6932c3ae3912 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
   299
### ?y = .x
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5132
diff changeset
   300
Goal "[| P y; !!x. P x ==> x = y |] ==> (@(x',y). x = x' & P y) = (x,y)";
4534
6932c3ae3912 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
   301
by (rtac select_equality 1);
6932c3ae3912 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
   302
by ( Simp_tac 1);
6932c3ae3912 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
   303
by (split_all_tac 1);
6932c3ae3912 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
   304
by (Asm_full_simp_tac 1);
6932c3ae3912 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
   305
qed "Eps_split_eq";
6932c3ae3912 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
   306
*)
6932c3ae3912 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
   307
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   308
(*** prod_fun -- action of the product functor upon functions ***)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   309
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4989
diff changeset
   310
Goalw [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   311
by (rtac split 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   312
qed "prod_fun";
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4435
diff changeset
   313
Addsimps [prod_fun];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   314
5278
a903b66822e2 even more tidying of Goal commands
paulson
parents: 5144
diff changeset
   315
Goal "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   316
by (rtac ext 1);
4828
ee3317896a47 improved split_all_tac significantly
oheimb
parents: 4819
diff changeset
   317
by (pair_tac "x" 1);
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4435
diff changeset
   318
by (Asm_simp_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   319
qed "prod_fun_compose";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   320
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4989
diff changeset
   321
Goal "prod_fun (%x. x) (%y. y) = (%z. z)";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   322
by (rtac ext 1);
4828
ee3317896a47 improved split_all_tac significantly
oheimb
parents: 4819
diff changeset
   323
by (pair_tac "z" 1);
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4435
diff changeset
   324
by (Asm_simp_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   325
qed "prod_fun_ident";
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4435
diff changeset
   326
Addsimps [prod_fun_ident];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   327
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5303
diff changeset
   328
Goal "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   329
by (rtac image_eqI 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   330
by (rtac (prod_fun RS sym) 1);
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5303
diff changeset
   331
by (assume_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   332
qed "prod_fun_imageI";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   333
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5303
diff changeset
   334
val major::prems = Goal
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 923
diff changeset
   335
    "[| c: (prod_fun f g)``r;  !!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P  \
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   336
\    |] ==> P";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   337
by (rtac (major RS imageE) 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   338
by (res_inst_tac [("p","x")] PairE 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   339
by (resolve_tac prems 1);
2935
998cb95fdd43 Yet more fast_tac->blast_tac, and other tidying
paulson
parents: 2886
diff changeset
   340
by (Blast_tac 2);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   341
by (blast_tac (claset() addIs [prod_fun]) 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   342
qed "prod_fun_imageE";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   343
5788
e3a98a7c0634 Domain r, Range r replace fst``r, snd``r
paulson
parents: 5761
diff changeset
   344
AddIs  [prod_fun_imageI];
e3a98a7c0634 Domain r, Range r replace fst``r, snd``r
paulson
parents: 5761
diff changeset
   345
AddSEs [prod_fun_imageE];
e3a98a7c0634 Domain r, Range r replace fst``r, snd``r
paulson
parents: 5761
diff changeset
   346
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4435
diff changeset
   347
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   348
(*** Disjoint union of a family of sets - Sigma ***)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   349
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   350
Goalw [Sigma_def] "[| a:A;  b:B(a) |] ==> (a,b) : Sigma A B";
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   351
by (REPEAT (ares_tac [singletonI,UN_I] 1));
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   352
qed "SigmaI";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   353
2856
cdb908486a96 Reorganization of how classical rules are installed
paulson
parents: 2637
diff changeset
   354
AddSIs [SigmaI];
cdb908486a96 Reorganization of how classical rules are installed
paulson
parents: 2637
diff changeset
   355
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   356
(*The general elimination rule*)
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   357
val major::prems = Goalw [Sigma_def]
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   358
    "[| c: Sigma A B;  \
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 923
diff changeset
   359
\       !!x y.[| x:A;  y:B(x);  c=(x,y) |] ==> P \
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   360
\    |] ==> P";
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   361
by (cut_facts_tac [major] 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   362
by (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ;
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   363
qed "SigmaE";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   364
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 923
diff changeset
   365
(** Elimination of (a,b):A*B -- introduces no eigenvariables **)
7007
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6830
diff changeset
   366
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6830
diff changeset
   367
Goal "(a,b) : Sigma A B ==> a : A";
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6830
diff changeset
   368
by (etac SigmaE 1);
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6830
diff changeset
   369
by (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ;
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6830
diff changeset
   370
qed "SigmaD1";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   371
7007
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6830
diff changeset
   372
Goal "(a,b) : Sigma A B ==> b : B(a)";
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6830
diff changeset
   373
by (etac SigmaE 1);
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6830
diff changeset
   374
by (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ;
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6830
diff changeset
   375
qed "SigmaD2";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   376
7007
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6830
diff changeset
   377
val [major,minor]= goal Prod.thy
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 923
diff changeset
   378
    "[| (a,b) : Sigma A B;    \
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   379
\       [| a:A;  b:B(a) |] ==> P   \
7007
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6830
diff changeset
   380
\    |] ==> P";
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6830
diff changeset
   381
by (rtac minor 1);
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6830
diff changeset
   382
by (rtac (major RS SigmaD1) 1);
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6830
diff changeset
   383
by (rtac (major RS SigmaD2) 1) ;
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6830
diff changeset
   384
qed "SigmaE2";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   385
2856
cdb908486a96 Reorganization of how classical rules are installed
paulson
parents: 2637
diff changeset
   386
AddSEs [SigmaE2, SigmaE];
cdb908486a96 Reorganization of how classical rules are installed
paulson
parents: 2637
diff changeset
   387
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5303
diff changeset
   388
val prems = Goal
1642
21db0cf9a1a4 Using new "Times" infix
paulson
parents: 1618
diff changeset
   389
    "[| A<=C;  !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D";
1515
4ed79ebab64d Introduced normalize_thm into HOL.ML
nipkow
parents: 1485
diff changeset
   390
by (cut_facts_tac prems 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   391
by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
1515
4ed79ebab64d Introduced normalize_thm into HOL.ML
nipkow
parents: 1485
diff changeset
   392
qed "Sigma_mono";
4ed79ebab64d Introduced normalize_thm into HOL.ML
nipkow
parents: 1485
diff changeset
   393
7007
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6830
diff changeset
   394
Goal "Sigma {} B = {}";
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6830
diff changeset
   395
by (Blast_tac 1) ;
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6830
diff changeset
   396
qed "Sigma_empty1";
1618
372880456b5b Library changes for mutilated checkerboard
paulson
parents: 1552
diff changeset
   397
7007
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6830
diff changeset
   398
Goal "A Times {} = {}";
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6830
diff changeset
   399
by (Blast_tac 1) ;
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6830
diff changeset
   400
qed "Sigma_empty2";
1618
372880456b5b Library changes for mutilated checkerboard
paulson
parents: 1552
diff changeset
   401
372880456b5b Library changes for mutilated checkerboard
paulson
parents: 1552
diff changeset
   402
Addsimps [Sigma_empty1,Sigma_empty2]; 
372880456b5b Library changes for mutilated checkerboard
paulson
parents: 1552
diff changeset
   403
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4989
diff changeset
   404
Goal "((a,b): Sigma A B) = (a:A & b:B(a))";
2935
998cb95fdd43 Yet more fast_tac->blast_tac, and other tidying
paulson
parents: 2886
diff changeset
   405
by (Blast_tac 1);
1618
372880456b5b Library changes for mutilated checkerboard
paulson
parents: 1552
diff changeset
   406
qed "mem_Sigma_iff";
3568
36ff1ab12021 Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents: 3429
diff changeset
   407
AddIffs [mem_Sigma_iff]; 
1618
372880456b5b Library changes for mutilated checkerboard
paulson
parents: 1552
diff changeset
   408
6016
797c76d6ff04 new (and generalized) theorems about Sigma/Times
paulson
parents: 5810
diff changeset
   409
Goal "x:C ==> (A Times C <= B Times C) = (A <= B)";
797c76d6ff04 new (and generalized) theorems about Sigma/Times
paulson
parents: 5810
diff changeset
   410
by (Blast_tac 1);
797c76d6ff04 new (and generalized) theorems about Sigma/Times
paulson
parents: 5810
diff changeset
   411
qed "Times_subset_cancel2";
797c76d6ff04 new (and generalized) theorems about Sigma/Times
paulson
parents: 5810
diff changeset
   412
797c76d6ff04 new (and generalized) theorems about Sigma/Times
paulson
parents: 5810
diff changeset
   413
Goal "x:C ==> (A Times C = B Times C) = (A = B)";
797c76d6ff04 new (and generalized) theorems about Sigma/Times
paulson
parents: 5810
diff changeset
   414
by (blast_tac (claset() addEs [equalityE]) 1);
797c76d6ff04 new (and generalized) theorems about Sigma/Times
paulson
parents: 5810
diff changeset
   415
qed "Times_eq_cancel2";
797c76d6ff04 new (and generalized) theorems about Sigma/Times
paulson
parents: 5810
diff changeset
   416
5810
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   417
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   418
(*** Complex rules for Sigma ***)
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   419
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   420
Goal "{(a,b). P a & Q b} = Collect P Times Collect Q";
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   421
by (Blast_tac 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   422
qed "Collect_split";
972b5f62f476 getting rid of qed_goal
paulson
parents: 7007
diff changeset
   423
4534
6932c3ae3912 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
   424
Addsimps [Collect_split];
1515
4ed79ebab64d Introduced normalize_thm into HOL.ML
nipkow
parents: 1485
diff changeset
   425
2856
cdb908486a96 Reorganization of how classical rules are installed
paulson
parents: 2637
diff changeset
   426
(*Suggested by Pierre Chartier*)
5278
a903b66822e2 even more tidying of Goal commands
paulson
parents: 5144
diff changeset
   427
Goal "(UN (a,b):(A Times B). E a Times F b) = (UNION A E) Times (UNION B F)";
2935
998cb95fdd43 Yet more fast_tac->blast_tac, and other tidying
paulson
parents: 2886
diff changeset
   428
by (Blast_tac 1);
6830
f8aed3706af7 renamed UNION_... to UN_... (to fit the convention)
paulson
parents: 6394
diff changeset
   429
qed "UN_Times_distrib";
2856
cdb908486a96 Reorganization of how classical rules are installed
paulson
parents: 2637
diff changeset
   430
6016
797c76d6ff04 new (and generalized) theorems about Sigma/Times
paulson
parents: 5810
diff changeset
   431
Goal "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))";
5810
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   432
by (Fast_tac 1);
6016
797c76d6ff04 new (and generalized) theorems about Sigma/Times
paulson
parents: 5810
diff changeset
   433
qed "split_paired_Ball_Sigma";
797c76d6ff04 new (and generalized) theorems about Sigma/Times
paulson
parents: 5810
diff changeset
   434
Addsimps [split_paired_Ball_Sigma];
5810
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   435
6016
797c76d6ff04 new (and generalized) theorems about Sigma/Times
paulson
parents: 5810
diff changeset
   436
Goal "(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))";
5810
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   437
by (Fast_tac 1);
6016
797c76d6ff04 new (and generalized) theorems about Sigma/Times
paulson
parents: 5810
diff changeset
   438
qed "split_paired_Bex_Sigma";
797c76d6ff04 new (and generalized) theorems about Sigma/Times
paulson
parents: 5810
diff changeset
   439
Addsimps [split_paired_Bex_Sigma];
5810
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   440
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   441
Goal "(SIGMA i:I Un J. C(i)) = (SIGMA i:I. C(i)) Un (SIGMA j:J. C(j))";
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   442
by (Blast_tac 1);
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   443
qed "Sigma_Un_distrib1";
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   444
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   445
Goal "(SIGMA i:I. A(i) Un B(i)) = (SIGMA i:I. A(i)) Un (SIGMA i:I. B(i))";
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   446
by (Blast_tac 1);
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   447
qed "Sigma_Un_distrib2";
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   448
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   449
Goal "(SIGMA i:I Int J. C(i)) = (SIGMA i:I. C(i)) Int (SIGMA j:J. C(j))";
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   450
by (Blast_tac 1);
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   451
qed "Sigma_Int_distrib1";
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   452
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   453
Goal "(SIGMA i:I. A(i) Int B(i)) = (SIGMA i:I. A(i)) Int (SIGMA i:I. B(i))";
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   454
by (Blast_tac 1);
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   455
qed "Sigma_Int_distrib2";
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   456
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   457
Goal "(SIGMA i:I - J. C(i)) = (SIGMA i:I. C(i)) - (SIGMA j:J. C(j))";
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   458
by (Blast_tac 1);
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   459
qed "Sigma_Diff_distrib1";
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   460
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   461
Goal "(SIGMA i:I. A(i) - B(i)) = (SIGMA i:I. A(i)) - (SIGMA i:I. B(i))";
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   462
by (Blast_tac 1);
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   463
qed "Sigma_Diff_distrib2";
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   464
6016
797c76d6ff04 new (and generalized) theorems about Sigma/Times
paulson
parents: 5810
diff changeset
   465
Goal "Sigma (Union X) B = (UN A:X. Sigma A B)";
797c76d6ff04 new (and generalized) theorems about Sigma/Times
paulson
parents: 5810
diff changeset
   466
by (Blast_tac 1);
797c76d6ff04 new (and generalized) theorems about Sigma/Times
paulson
parents: 5810
diff changeset
   467
qed "Sigma_Union";
797c76d6ff04 new (and generalized) theorems about Sigma/Times
paulson
parents: 5810
diff changeset
   468
8255
38f96394c099 new distributive laws
paulson
parents: 8157
diff changeset
   469
(*Non-dependent versions are needed to avoid the need for higher-order
38f96394c099 new distributive laws
paulson
parents: 8157
diff changeset
   470
  matching, especially when the rules are re-oriented*)
38f96394c099 new distributive laws
paulson
parents: 8157
diff changeset
   471
Goal "(A Un B) Times C = (A Times C) Un (B Times C)";
38f96394c099 new distributive laws
paulson
parents: 8157
diff changeset
   472
by (Blast_tac 1);
38f96394c099 new distributive laws
paulson
parents: 8157
diff changeset
   473
qed "Times_Un_distrib1"; 
38f96394c099 new distributive laws
paulson
parents: 8157
diff changeset
   474
38f96394c099 new distributive laws
paulson
parents: 8157
diff changeset
   475
Goal "(A Int B) Times C = (A Times C) Int (B Times C)";
38f96394c099 new distributive laws
paulson
parents: 8157
diff changeset
   476
by (Blast_tac 1);
38f96394c099 new distributive laws
paulson
parents: 8157
diff changeset
   477
qed "Times_Int_distrib1"; 
38f96394c099 new distributive laws
paulson
parents: 8157
diff changeset
   478
38f96394c099 new distributive laws
paulson
parents: 8157
diff changeset
   479
Goal "(A - B) Times C = (A Times C) - (B Times C)";
38f96394c099 new distributive laws
paulson
parents: 8157
diff changeset
   480
by (Blast_tac 1);
38f96394c099 new distributive laws
paulson
parents: 8157
diff changeset
   481
qed "Times_Diff_distrib1"; 
5810
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   482
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   483
(** Exhaustion rule for unit -- a degenerate form of induction **)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   484
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4989
diff changeset
   485
Goalw [Unity_def]
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 923
diff changeset
   486
    "u = ()";
2886
fd5645efa43d Now: unit = {True}
nipkow
parents: 2880
diff changeset
   487
by (stac (rewrite_rule [unit_def] Rep_unit RS singletonD RS sym) 1);
2880
a0fde30aa126 Removed (Unit) in Prod.
nipkow
parents: 2856
diff changeset
   488
by (rtac (Rep_unit_inverse RS sym) 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   489
qed "unit_eq";
1754
852093aeb0ab Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents: 1746
diff changeset
   490
 
5088
e4aa78d1312f New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents: 5083
diff changeset
   491
(*simplification procedure for unit_eq.
e4aa78d1312f New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents: 5083
diff changeset
   492
  Cannot use this rule directly -- it loops!*)
5083
beb21c000cb1 added unit_eq simplification procedure;
wenzelm
parents: 5069
diff changeset
   493
local
6394
3d9fd50fcc43 Theory.sign_of;
wenzelm
parents: 6016
diff changeset
   494
  val unit_pat = Thm.cterm_of (Theory.sign_of thy) (Free ("x", HOLogic.unitT));
5553
ae42b36a50c2 renamed mk_meta_eq to mk_eq
oheimb
parents: 5361
diff changeset
   495
  val unit_meta_eq = standard (mk_meta_eq unit_eq);
5083
beb21c000cb1 added unit_eq simplification procedure;
wenzelm
parents: 5069
diff changeset
   496
  fun proc _ _ t =
beb21c000cb1 added unit_eq simplification procedure;
wenzelm
parents: 5069
diff changeset
   497
    if HOLogic.is_unit t then None
beb21c000cb1 added unit_eq simplification procedure;
wenzelm
parents: 5069
diff changeset
   498
    else Some unit_meta_eq;
beb21c000cb1 added unit_eq simplification procedure;
wenzelm
parents: 5069
diff changeset
   499
in
beb21c000cb1 added unit_eq simplification procedure;
wenzelm
parents: 5069
diff changeset
   500
  val unit_eq_proc = Simplifier.mk_simproc "unit_eq" [unit_pat] proc;
beb21c000cb1 added unit_eq simplification procedure;
wenzelm
parents: 5069
diff changeset
   501
end;
beb21c000cb1 added unit_eq simplification procedure;
wenzelm
parents: 5069
diff changeset
   502
beb21c000cb1 added unit_eq simplification procedure;
wenzelm
parents: 5069
diff changeset
   503
Addsimprocs [unit_eq_proc];
beb21c000cb1 added unit_eq simplification procedure;
wenzelm
parents: 5069
diff changeset
   504
beb21c000cb1 added unit_eq simplification procedure;
wenzelm
parents: 5069
diff changeset
   505
5761
a396eff81fda Added theorem unit_induct (for rep_datatype).
berghofe
parents: 5715
diff changeset
   506
Goal "P () ==> P x";
a396eff81fda Added theorem unit_induct (for rep_datatype).
berghofe
parents: 5715
diff changeset
   507
by (Simp_tac 1);
a396eff81fda Added theorem unit_induct (for rep_datatype).
berghofe
parents: 5715
diff changeset
   508
qed "unit_induct";
a396eff81fda Added theorem unit_induct (for rep_datatype).
berghofe
parents: 5715
diff changeset
   509
a396eff81fda Added theorem unit_induct (for rep_datatype).
berghofe
parents: 5715
diff changeset
   510
5088
e4aa78d1312f New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents: 5083
diff changeset
   511
(*This rewrite counters the effect of unit_eq_proc on (%u::unit. f u),
e4aa78d1312f New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents: 5083
diff changeset
   512
  replacing it by f rather than by %u.f(). *)
e4aa78d1312f New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents: 5083
diff changeset
   513
Goal "(%u::unit. f()) = f";
e4aa78d1312f New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents: 5083
diff changeset
   514
by (rtac ext 1);
e4aa78d1312f New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents: 5083
diff changeset
   515
by (Simp_tac 1);
e4aa78d1312f New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents: 5083
diff changeset
   516
qed "unit_abs_eta_conv";
e4aa78d1312f New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents: 5083
diff changeset
   517
Addsimps [unit_abs_eta_conv];
e4aa78d1312f New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents: 5083
diff changeset
   518
e4aa78d1312f New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents: 5083
diff changeset
   519
5096
84b00be693b4 Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents: 5088
diff changeset
   520
(*Attempts to remove occurrences of split, and pair-valued parameters*)
84b00be693b4 Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents: 5088
diff changeset
   521
val remove_split = rewrite_rule [split RS eq_reflection] o  
84b00be693b4 Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents: 5088
diff changeset
   522
                   rule_by_tactic (TRYALL split_all_tac);
1746
f0c6aabc6c02 Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents: 1727
diff changeset
   523
5096
84b00be693b4 Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents: 5088
diff changeset
   524
local
1746
f0c6aabc6c02 Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents: 1727
diff changeset
   525
f0c6aabc6c02 Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents: 1727
diff changeset
   526
(*In ap_split S T u, term u expects separate arguments for the factors of S,
f0c6aabc6c02 Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents: 1727
diff changeset
   527
  with result type T.  The call creates a new term expecting one argument
f0c6aabc6c02 Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents: 1727
diff changeset
   528
  of type S.*)
5096
84b00be693b4 Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents: 5088
diff changeset
   529
fun ap_split (Type ("*", [T1, T2])) T3 u = 
84b00be693b4 Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents: 5088
diff changeset
   530
      HOLogic.split_const (T1, T2, T3) $ 
1746
f0c6aabc6c02 Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents: 1727
diff changeset
   531
      Abs("v", T1, 
2031
03a843f0f447 Ran expandshort
paulson
parents: 1754
diff changeset
   532
          ap_split T2 T3
5096
84b00be693b4 Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents: 5088
diff changeset
   533
             ((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $ 
2031
03a843f0f447 Ran expandshort
paulson
parents: 1754
diff changeset
   534
              Bound 0))
1746
f0c6aabc6c02 Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents: 1727
diff changeset
   535
  | ap_split T T3 u = u;
f0c6aabc6c02 Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents: 1727
diff changeset
   536
5096
84b00be693b4 Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents: 5088
diff changeset
   537
(*Curries any Var of function type in the rule*)
84b00be693b4 Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents: 5088
diff changeset
   538
fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2])), rl) =
84b00be693b4 Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents: 5088
diff changeset
   539
      let val T' = HOLogic.prodT_factors T1 ---> T2
84b00be693b4 Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents: 5088
diff changeset
   540
          val newt = ap_split T1 T2 (Var (v, T'))
84b00be693b4 Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents: 5088
diff changeset
   541
          val cterm = Thm.cterm_of (#sign (rep_thm rl))
84b00be693b4 Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents: 5088
diff changeset
   542
      in
84b00be693b4 Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents: 5088
diff changeset
   543
          instantiate ([], [(cterm t, cterm newt)]) rl
84b00be693b4 Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents: 5088
diff changeset
   544
      end
84b00be693b4 Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents: 5088
diff changeset
   545
  | split_rule_var' (t, rl) = rl;
1746
f0c6aabc6c02 Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents: 1727
diff changeset
   546
5096
84b00be693b4 Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents: 5088
diff changeset
   547
in
1746
f0c6aabc6c02 Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents: 1727
diff changeset
   548
5096
84b00be693b4 Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents: 5088
diff changeset
   549
val split_rule_var = standard o remove_split o split_rule_var';
84b00be693b4 Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents: 5088
diff changeset
   550
84b00be693b4 Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents: 5088
diff changeset
   551
(*Curries ALL function variables occurring in a rule's conclusion*)
84b00be693b4 Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents: 5088
diff changeset
   552
fun split_rule rl = remove_split (foldr split_rule_var' (term_vars (concl_of rl), rl))
1746
f0c6aabc6c02 Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents: 1727
diff changeset
   553
                    |> standard;
f0c6aabc6c02 Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents: 1727
diff changeset
   554
f0c6aabc6c02 Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents: 1727
diff changeset
   555
end;
5810
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   556
829cae93f132 new TIMES/Sigma rules
paulson
parents: 5788
diff changeset
   557