QuotMain.thy
author Christian Urban <urbanc@in.tum.de>
Mon, 07 Dec 2009 01:22:20 +0100
changeset 588 2c95d0436a2b
parent 586 cdc6ae1a4ed2
child 589 4e66a18f263b
permissions -rw-r--r--
removed usage of HOL_basic_ss by using a slighly extended version of empty_ss
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
theory QuotMain
6
6a1b4c22a386 added the prove command
Christian Urban <urbanc@in.tum.de>
parents: 5
diff changeset
     2
imports QuotScript QuotList Prove
544
c15eea8d20af Minor renames and moving
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 543
diff changeset
     3
uses ("quotient_info.ML")
264
d0581fbc096c split quotient.ML into two files
Christian Urban <urbanc@in.tum.de>
parents: 263
diff changeset
     4
     ("quotient.ML")
277
37636f2b1c19 separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents: 275
diff changeset
     5
     ("quotient_def.ML")
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
begin
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     7
582
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
     8
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     9
locale QUOT_TYPE =
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    10
  fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    11
  and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    12
  and   Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
582
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
    13
  assumes equivp: "equivp R"
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    14
  and     rep_prop: "\<And>y. \<exists>x. Rep y = R x"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    15
  and     rep_inverse: "\<And>x. Abs (Rep x) = x"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    16
  and     abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    17
  and     rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
15
f46eddb570a3 Cleaning the code
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 14
diff changeset
    18
begin
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    19
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    20
definition
200
d6a24dad5882 made quotients compatiple with Nominal; updated keyword file
Christian Urban <urbanc@in.tum.de>
parents: 198
diff changeset
    21
  ABS::"'a \<Rightarrow> 'b"
d6a24dad5882 made quotients compatiple with Nominal; updated keyword file
Christian Urban <urbanc@in.tum.de>
parents: 198
diff changeset
    22
where
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    23
  "ABS x \<equiv> Abs (R x)"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    24
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    25
definition
200
d6a24dad5882 made quotients compatiple with Nominal; updated keyword file
Christian Urban <urbanc@in.tum.de>
parents: 198
diff changeset
    26
  REP::"'b \<Rightarrow> 'a"
d6a24dad5882 made quotients compatiple with Nominal; updated keyword file
Christian Urban <urbanc@in.tum.de>
parents: 198
diff changeset
    27
where
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    28
  "REP a = Eps (Rep a)"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    29
15
f46eddb570a3 Cleaning the code
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 14
diff changeset
    30
lemma lem9:
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    31
  shows "R (Eps (R x)) = R x"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    32
proof -
582
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
    33
  have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def)
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    34
  then have "R x (Eps (R x))" by (rule someI)
15
f46eddb570a3 Cleaning the code
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 14
diff changeset
    35
  then show "R (Eps (R x)) = R x"
582
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
    36
    using equivp unfolding equivp_def by simp
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    37
qed
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    38
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    39
theorem thm10:
24
6885fa184e89 Merged with my changes from the morning:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 23
diff changeset
    40
  shows "ABS (REP a) \<equiv> a"
6885fa184e89 Merged with my changes from the morning:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 23
diff changeset
    41
  apply  (rule eq_reflection)
6885fa184e89 Merged with my changes from the morning:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 23
diff changeset
    42
  unfolding ABS_def REP_def
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    43
proof -
15
f46eddb570a3 Cleaning the code
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 14
diff changeset
    44
  from rep_prop
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    45
  obtain x where eq: "Rep a = R x" by auto
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    46
  have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    47
  also have "\<dots> = Abs (R x)" using lem9 by simp
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    48
  also have "\<dots> = Abs (Rep a)" using eq by simp
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    49
  also have "\<dots> = a" using rep_inverse by simp
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    50
  finally
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    51
  show "Abs (R (Eps (Rep a))) = a" by simp
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    52
qed
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    53
15
f46eddb570a3 Cleaning the code
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 14
diff changeset
    54
lemma REP_refl:
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    55
  shows "R (REP a) (REP a)"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    56
unfolding REP_def
582
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
    57
by (simp add: equivp[simplified equivp_def])
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    58
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    59
lemma lem7:
22
5023bf36d81a beautification of some proofs
Ning@localhost
parents: 21
diff changeset
    60
  shows "(R x = R y) = (Abs (R x) = Abs (R y))"
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    61
apply(rule iffI)
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    62
apply(simp)
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    63
apply(drule rep_inject[THEN iffD2])
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    64
apply(simp add: abs_inverse)
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    65
done
15
f46eddb570a3 Cleaning the code
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 14
diff changeset
    66
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    67
theorem thm11:
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    68
  shows "R r r' = (ABS r = ABS r')"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    69
unfolding ABS_def
582
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
    70
by (simp only: equivp[simplified equivp_def] lem7)
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    71
4
Christian Urban <urbanc@in.tum.de>
parents: 3
diff changeset
    72
2
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
    73
lemma REP_ABS_rsp:
4
Christian Urban <urbanc@in.tum.de>
parents: 3
diff changeset
    74
  shows "R f (REP (ABS g)) = R f g"
Christian Urban <urbanc@in.tum.de>
parents: 3
diff changeset
    75
  and   "R (REP (ABS g)) f = R g f"
23
f6c6cf8c3b98 some more beautification
Ning@localhost
parents: 22
diff changeset
    76
by (simp_all add: thm10 thm11)
4
Christian Urban <urbanc@in.tum.de>
parents: 3
diff changeset
    77
529
6348c2a57ec2 More name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 527
diff changeset
    78
lemma Quotient:
6348c2a57ec2 More name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 527
diff changeset
    79
  "Quotient R ABS REP"
6348c2a57ec2 More name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 527
diff changeset
    80
apply(unfold Quotient_def)
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    81
apply(simp add: thm10)
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    82
apply(simp add: REP_refl)
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    83
apply(subst thm11[symmetric])
582
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
    84
apply(simp add: equivp[simplified equivp_def])
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    85
done
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    86
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
    87
lemma R_trans:
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
    88
  assumes ab: "R a b"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
    89
  and     bc: "R b c"
22
5023bf36d81a beautification of some proofs
Ning@localhost
parents: 21
diff changeset
    90
  shows "R a c"
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
    91
proof -
582
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
    92
  have tr: "transp R" using equivp equivp_reflp_symp_transp[of R] by simp
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
    93
  moreover have ab: "R a b" by fact
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
    94
  moreover have bc: "R b c" by fact
529
6348c2a57ec2 More name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 527
diff changeset
    95
  ultimately show "R a c" unfolding transp_def by blast
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
    96
qed
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
    97
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
    98
lemma R_sym:
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
    99
  assumes ab: "R a b"
22
5023bf36d81a beautification of some proofs
Ning@localhost
parents: 21
diff changeset
   100
  shows "R b a"
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   101
proof -
582
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   102
  have re: "symp R" using equivp equivp_reflp_symp_transp[of R] by simp
529
6348c2a57ec2 More name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 527
diff changeset
   103
  then show "R b a" using ab unfolding symp_def by blast
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   104
qed
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   105
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   106
lemma R_trans2:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   107
  assumes ac: "R a c"
22
5023bf36d81a beautification of some proofs
Ning@localhost
parents: 21
diff changeset
   108
  and     bd: "R b d"
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   109
  shows "R a b = R c d"
200
d6a24dad5882 made quotients compatiple with Nominal; updated keyword file
Christian Urban <urbanc@in.tum.de>
parents: 198
diff changeset
   110
using ac bd
d6a24dad5882 made quotients compatiple with Nominal; updated keyword file
Christian Urban <urbanc@in.tum.de>
parents: 198
diff changeset
   111
by (blast intro: R_trans R_sym)
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   112
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   113
lemma REPS_same:
25
9020ee23a020 The tactic with REPEAT, CHANGED and a proper simpset.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 24
diff changeset
   114
  shows "R (REP a) (REP b) \<equiv> (a = b)"
38
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   115
proof -
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   116
  have "R (REP a) (REP b) = (a = b)"
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   117
  proof
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   118
    assume as: "R (REP a) (REP b)"
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   119
    from rep_prop
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   120
    obtain x y
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   121
      where eqs: "Rep a = R x" "Rep b = R y" by blast
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   122
    from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   123
    then have "R x (Eps (R y))" using lem9 by simp
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   124
    then have "R (Eps (R y)) x" using R_sym by blast
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   125
    then have "R y x" using lem9 by simp
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   126
    then have "R x y" using R_sym by blast
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   127
    then have "ABS x = ABS y" using thm11 by simp
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   128
    then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   129
    then show "a = b" using rep_inverse by simp
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   130
  next
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   131
    assume ab: "a = b"
582
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   132
    have "reflp R" using equivp equivp_reflp_symp_transp[of R] by simp
529
6348c2a57ec2 More name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 527
diff changeset
   133
    then show "R (REP a) (REP b)" unfolding reflp_def using ab by auto
38
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   134
  qed
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   135
  then show "R (REP a) (REP b) \<equiv> (a = b)" by simp
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   136
qed
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   137
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   138
end
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   139
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   140
section {* type definition for the quotient type *}
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   141
268
4d58c02289ca simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   142
(* the auxiliary data for the quotient types *)
264
d0581fbc096c split quotient.ML into two files
Christian Urban <urbanc@in.tum.de>
parents: 263
diff changeset
   143
use "quotient_info.ML"
268
4d58c02289ca simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   144
537
57073b0b8fac Even more name changes and cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 536
diff changeset
   145
declare [[map list = (map, list_rel)]]
185
929bc55efff7 added code for declaring map-functions
Christian Urban <urbanc@in.tum.de>
parents: 182
diff changeset
   146
declare [[map * = (prod_fun, prod_rel)]]
536
44fa9df44e6f More code cleaning and name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 529
diff changeset
   147
declare [[map "fun" = (fun_map, fun_rel)]]
185
929bc55efff7 added code for declaring map-functions
Christian Urban <urbanc@in.tum.de>
parents: 182
diff changeset
   148
537
57073b0b8fac Even more name changes and cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 536
diff changeset
   149
lemmas [quotient_thm] =
57073b0b8fac Even more name changes and cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 536
diff changeset
   150
  fun_quotient list_quotient
506
91c374abde06 removed quot argument...not all examples work anymore
Christian Urban <urbanc@in.tum.de>
parents: 505
diff changeset
   151
555
b460565dbb58 Handling of respects in the fast inj_repabs_tac; includes respects with quotient assumptions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 554
diff changeset
   152
lemmas [quotient_rsp] =
566
4eca2c3e59f7 Used symmetric definitions. Moved quotient_rsp to QuotMain.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 564
diff changeset
   153
  quot_rel_rsp nil_rsp cons_rsp foldl_rsp
555
b460565dbb58 Handling of respects in the fast inj_repabs_tac; includes respects with quotient assumptions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 554
diff changeset
   154
582
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   155
(* OPTION, PRODUCTS *)
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   156
lemmas [quotient_equiv] =
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   157
  identity_equivp list_equivp
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   158
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   159
185
929bc55efff7 added code for declaring map-functions
Christian Urban <urbanc@in.tum.de>
parents: 182
diff changeset
   160
ML {* maps_lookup @{theory} "List.list" *}
929bc55efff7 added code for declaring map-functions
Christian Urban <urbanc@in.tum.de>
parents: 182
diff changeset
   161
ML {* maps_lookup @{theory} "*" *}
929bc55efff7 added code for declaring map-functions
Christian Urban <urbanc@in.tum.de>
parents: 182
diff changeset
   162
ML {* maps_lookup @{theory} "fun" *}
174
09048a951dca moved the map_funs setup into QuotMain
Christian Urban <urbanc@in.tum.de>
parents: 170
diff changeset
   163
268
4d58c02289ca simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   164
4d58c02289ca simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   165
(* definition of the quotient types *)
277
37636f2b1c19 separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents: 275
diff changeset
   166
(* FIXME: should be called quotient_typ.ML *)
268
4d58c02289ca simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   167
use "quotient.ML"
4d58c02289ca simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   168
4d58c02289ca simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   169
277
37636f2b1c19 separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents: 275
diff changeset
   170
(* lifting of constants *)
37636f2b1c19 separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents: 275
diff changeset
   171
use "quotient_def.ML"
37636f2b1c19 separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents: 275
diff changeset
   172
588
2c95d0436a2b removed usage of HOL_basic_ss by using a slighly extended version of empty_ss
Christian Urban <urbanc@in.tum.de>
parents: 586
diff changeset
   173
section {* Bounded abstraction *}
2c95d0436a2b removed usage of HOL_basic_ss by using a slighly extended version of empty_ss
Christian Urban <urbanc@in.tum.de>
parents: 586
diff changeset
   174
381
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   175
definition
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   176
  Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   177
where
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   178
  "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
310
fec6301a1989 added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   179
588
2c95d0436a2b removed usage of HOL_basic_ss by using a slighly extended version of empty_ss
Christian Urban <urbanc@in.tum.de>
parents: 586
diff changeset
   180
section {* Simset setup *}
2c95d0436a2b removed usage of HOL_basic_ss by using a slighly extended version of empty_ss
Christian Urban <urbanc@in.tum.de>
parents: 586
diff changeset
   181
2c95d0436a2b removed usage of HOL_basic_ss by using a slighly extended version of empty_ss
Christian Urban <urbanc@in.tum.de>
parents: 586
diff changeset
   182
(* since HOL_basic_ss is too "big", we need to set up *)
2c95d0436a2b removed usage of HOL_basic_ss by using a slighly extended version of empty_ss
Christian Urban <urbanc@in.tum.de>
parents: 586
diff changeset
   183
(* our own minimal simpset                            *)
2c95d0436a2b removed usage of HOL_basic_ss by using a slighly extended version of empty_ss
Christian Urban <urbanc@in.tum.de>
parents: 586
diff changeset
   184
ML {*
2c95d0436a2b removed usage of HOL_basic_ss by using a slighly extended version of empty_ss
Christian Urban <urbanc@in.tum.de>
parents: 586
diff changeset
   185
fun  mk_minimal_ss ctxt =
2c95d0436a2b removed usage of HOL_basic_ss by using a slighly extended version of empty_ss
Christian Urban <urbanc@in.tum.de>
parents: 586
diff changeset
   186
  Simplifier.context ctxt empty_ss
2c95d0436a2b removed usage of HOL_basic_ss by using a slighly extended version of empty_ss
Christian Urban <urbanc@in.tum.de>
parents: 586
diff changeset
   187
    setsubgoaler asm_simp_tac
2c95d0436a2b removed usage of HOL_basic_ss by using a slighly extended version of empty_ss
Christian Urban <urbanc@in.tum.de>
parents: 586
diff changeset
   188
    setmksimps (mksimps [])
2c95d0436a2b removed usage of HOL_basic_ss by using a slighly extended version of empty_ss
Christian Urban <urbanc@in.tum.de>
parents: 586
diff changeset
   189
*}
2c95d0436a2b removed usage of HOL_basic_ss by using a slighly extended version of empty_ss
Christian Urban <urbanc@in.tum.de>
parents: 586
diff changeset
   190
544
c15eea8d20af Minor renames and moving
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 543
diff changeset
   191
section {* atomize *}
139
4cc5db28b1c3 Reordering
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 138
diff changeset
   192
381
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   193
lemma atomize_eqv[atomize]:
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   194
  shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
139
4cc5db28b1c3 Reordering
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 138
diff changeset
   195
proof
381
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   196
  assume "A \<equiv> B"
139
4cc5db28b1c3 Reordering
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 138
diff changeset
   197
  then show "Trueprop A \<equiv> Trueprop B" by unfold
4cc5db28b1c3 Reordering
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 138
diff changeset
   198
next
4cc5db28b1c3 Reordering
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 138
diff changeset
   199
  assume *: "Trueprop A \<equiv> Trueprop B"
4cc5db28b1c3 Reordering
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 138
diff changeset
   200
  have "A = B"
4cc5db28b1c3 Reordering
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 138
diff changeset
   201
  proof (cases A)
4cc5db28b1c3 Reordering
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 138
diff changeset
   202
    case True
4cc5db28b1c3 Reordering
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 138
diff changeset
   203
    have "A" by fact
4cc5db28b1c3 Reordering
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 138
diff changeset
   204
    then show "A = B" using * by simp
4cc5db28b1c3 Reordering
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 138
diff changeset
   205
  next
4cc5db28b1c3 Reordering
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 138
diff changeset
   206
    case False
4cc5db28b1c3 Reordering
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 138
diff changeset
   207
    have "\<not>A" by fact
4cc5db28b1c3 Reordering
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 138
diff changeset
   208
    then show "A = B" using * by auto
4cc5db28b1c3 Reordering
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 138
diff changeset
   209
  qed
4cc5db28b1c3 Reordering
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 138
diff changeset
   210
  then show "A \<equiv> B" by (rule eq_reflection)
4cc5db28b1c3 Reordering
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 138
diff changeset
   211
qed
4cc5db28b1c3 Reordering
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 138
diff changeset
   212
4cc5db28b1c3 Reordering
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 138
diff changeset
   213
ML {*
4cc5db28b1c3 Reordering
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 138
diff changeset
   214
fun atomize_thm thm =
4cc5db28b1c3 Reordering
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 138
diff changeset
   215
let
221
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 219
diff changeset
   216
  val thm' = Thm.freezeT (forall_intr_vars thm)
139
4cc5db28b1c3 Reordering
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 138
diff changeset
   217
  val thm'' = ObjectLogic.atomize (cprop_of thm')
4cc5db28b1c3 Reordering
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 138
diff changeset
   218
in
404
d676974e3c89 more tuning
Christian Urban <urbanc@in.tum.de>
parents: 403
diff changeset
   219
  @{thm equal_elim_rule1} OF [thm'', thm']
139
4cc5db28b1c3 Reordering
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 138
diff changeset
   220
end
4cc5db28b1c3 Reordering
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 138
diff changeset
   221
*}
4cc5db28b1c3 Reordering
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 138
diff changeset
   222
387
f78aa16daae5 reordered the code
Christian Urban <urbanc@in.tum.de>
parents: 386
diff changeset
   223
section {* infrastructure about id *}
381
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   224
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   225
lemma prod_fun_id: "prod_fun id id \<equiv> id"
415
5a9bdf81672d More cleaning in QuotMain, identity handling.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 413
diff changeset
   226
  by (rule eq_reflection) (simp add: prod_fun_def)
381
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   227
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   228
lemma map_id: "map id \<equiv> id"
415
5a9bdf81672d More cleaning in QuotMain, identity handling.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 413
diff changeset
   229
  apply (rule eq_reflection)
5a9bdf81672d More cleaning in QuotMain, identity handling.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 413
diff changeset
   230
  apply (rule ext)
5a9bdf81672d More cleaning in QuotMain, identity handling.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 413
diff changeset
   231
  apply (rule_tac list="x" in list.induct)
5a9bdf81672d More cleaning in QuotMain, identity handling.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 413
diff changeset
   232
  apply (simp_all)
5a9bdf81672d More cleaning in QuotMain, identity handling.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 413
diff changeset
   233
  done
381
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   234
409
6b59a3844055 introduced a separate lemma for id_simps
Christian Urban <urbanc@in.tum.de>
parents: 408
diff changeset
   235
lemmas id_simps =
537
57073b0b8fac Even more name changes and cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 536
diff changeset
   236
  fun_map_id[THEN eq_reflection]
409
6b59a3844055 introduced a separate lemma for id_simps
Christian Urban <urbanc@in.tum.de>
parents: 408
diff changeset
   237
  id_apply[THEN eq_reflection]
415
5a9bdf81672d More cleaning in QuotMain, identity handling.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 413
diff changeset
   238
  id_def[THEN eq_reflection,symmetric]
5a9bdf81672d More cleaning in QuotMain, identity handling.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 413
diff changeset
   239
  prod_fun_id map_id
409
6b59a3844055 introduced a separate lemma for id_simps
Christian Urban <urbanc@in.tum.de>
parents: 408
diff changeset
   240
381
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   241
ML {*
409
6b59a3844055 introduced a separate lemma for id_simps
Christian Urban <urbanc@in.tum.de>
parents: 408
diff changeset
   242
fun simp_ids thm =
6b59a3844055 introduced a separate lemma for id_simps
Christian Urban <urbanc@in.tum.de>
parents: 408
diff changeset
   243
  MetaSimplifier.rewrite_rule @{thms id_simps} thm
381
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   244
*}
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   245
407
d387743f022b tuned comments and moved slightly some code
Christian Urban <urbanc@in.tum.de>
parents: 405
diff changeset
   246
section {* Debugging infrastructure for testing tactics *}
381
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   247
447
3e7ee6f5437d selective debugging of the inj_repabs_tac (at the moment for step 3 and 4 debugging information is printed)
Christian Urban <urbanc@in.tum.de>
parents: 446
diff changeset
   248
ML {*
450
2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents: 449
diff changeset
   249
fun my_print_tac ctxt s i thm =
407
d387743f022b tuned comments and moved slightly some code
Christian Urban <urbanc@in.tum.de>
parents: 405
diff changeset
   250
let
450
2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents: 449
diff changeset
   251
  val prem_str = nth (prems_of thm) (i - 1)
2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents: 449
diff changeset
   252
                 |> Syntax.string_of_term ctxt
2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents: 449
diff changeset
   253
                 handle Subscript => "no subgoal"
2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents: 449
diff changeset
   254
  val _ = tracing (s ^ "\n" ^ prem_str)
407
d387743f022b tuned comments and moved slightly some code
Christian Urban <urbanc@in.tum.de>
parents: 405
diff changeset
   255
in
d387743f022b tuned comments and moved slightly some code
Christian Urban <urbanc@in.tum.de>
parents: 405
diff changeset
   256
  Seq.single thm
450
2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents: 449
diff changeset
   257
end *}
2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents: 449
diff changeset
   258
447
3e7ee6f5437d selective debugging of the inj_repabs_tac (at the moment for step 3 and 4 debugging information is printed)
Christian Urban <urbanc@in.tum.de>
parents: 446
diff changeset
   259
ML {*
3e7ee6f5437d selective debugging of the inj_repabs_tac (at the moment for step 3 and 4 debugging information is printed)
Christian Urban <urbanc@in.tum.de>
parents: 446
diff changeset
   260
fun DT ctxt s tac i thm =
450
2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents: 449
diff changeset
   261
let
2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents: 449
diff changeset
   262
  val before_goal = nth (prems_of thm) (i - 1)
2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents: 449
diff changeset
   263
                    |> Syntax.string_of_term ctxt
2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents: 449
diff changeset
   264
  val before_msg = ["before: " ^ s, before_goal, "after: " ^ s]
2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents: 449
diff changeset
   265
                   |> cat_lines
2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents: 449
diff changeset
   266
in 
2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents: 449
diff changeset
   267
  EVERY [tac i, my_print_tac ctxt before_msg i] thm
2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents: 449
diff changeset
   268
end
444
Christian Urban <urbanc@in.tum.de>
parents: 443
diff changeset
   269
447
3e7ee6f5437d selective debugging of the inj_repabs_tac (at the moment for step 3 and 4 debugging information is printed)
Christian Urban <urbanc@in.tum.de>
parents: 446
diff changeset
   270
fun NDT ctxt s tac thm = tac thm  
407
d387743f022b tuned comments and moved slightly some code
Christian Urban <urbanc@in.tum.de>
parents: 405
diff changeset
   271
*}
d387743f022b tuned comments and moved slightly some code
Christian Urban <urbanc@in.tum.de>
parents: 405
diff changeset
   272
576
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   273
section {* Matching of terms and types *}
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   274
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   275
ML {*
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   276
fun matches_typ (ty, ty') =
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   277
  case (ty, ty') of
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   278
    (_, TVar _) => true
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   279
  | (TFree x, TFree x') => x = x'
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   280
  | (Type (s, tys), Type (s', tys')) => 
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   281
       s = s' andalso 
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   282
       if (length tys = length tys') 
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   283
       then (List.all matches_typ (tys ~~ tys')) 
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   284
       else false
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   285
  | _ => false
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   286
*}
577
8dab8d82f26b more tuning of the code
Christian Urban <urbanc@in.tum.de>
parents: 576
diff changeset
   287
576
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   288
ML {*
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   289
fun matches_term (trm, trm') = 
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   290
   case (trm, trm') of 
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   291
     (_, Var _) => true
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   292
   | (Const (s, ty), Const (s', ty')) => s = s' andalso matches_typ (ty, ty')
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   293
   | (Free (x, ty), Free (x', ty')) => x = x' andalso matches_typ (ty, ty')
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   294
   | (Bound i, Bound j) => i = j
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   295
   | (Abs (_, T, t), Abs (_, T', t')) => matches_typ (T, T') andalso matches_term (t, t')
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   296
   | (t $ s, t' $ s') => matches_term (t, t') andalso matches_term (s, s') 
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   297
   | _ => false
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   298
*}
453
c22ab554a32d started functions for qid-insertion and fixed a bug in regularise
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   299
407
d387743f022b tuned comments and moved slightly some code
Christian Urban <urbanc@in.tum.de>
parents: 405
diff changeset
   300
section {* Infrastructure for collecting theorems for starting the lifting *}
267
3764566c1151 Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 264
diff changeset
   301
3764566c1151 Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 264
diff changeset
   302
ML {*
239
02b14a21761a Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 236
diff changeset
   303
fun lookup_quot_data lthy qty =
02b14a21761a Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 236
diff changeset
   304
  let
311
77fc6f3c0343 changed the quotdata to be a symtab table (needs fixing)
Christian Urban <urbanc@in.tum.de>
parents: 310
diff changeset
   305
    val qty_name = fst (dest_Type qty)
314
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 311
diff changeset
   306
    val SOME quotdata = quotdata_lookup lthy qty_name
303
991b0e53f9dc More code cleaning and commenting
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 302
diff changeset
   307
    (* TODO: Should no longer be needed *)
257
68bd5c2a1b96 Fixed quotdata_lookup.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 255
diff changeset
   308
    val rty = Logic.unvarifyT (#rtyp quotdata)
239
02b14a21761a Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 236
diff changeset
   309
    val rel = #rel quotdata
02b14a21761a Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 236
diff changeset
   310
    val rel_eqv = #equiv_thm quotdata
529
6348c2a57ec2 More name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 527
diff changeset
   311
    val rel_refl = @{thm equivp_reflp} OF [rel_eqv]
239
02b14a21761a Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 236
diff changeset
   312
  in
02b14a21761a Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 236
diff changeset
   313
    (rty, rel, rel_refl, rel_eqv)
02b14a21761a Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 236
diff changeset
   314
  end
02b14a21761a Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 236
diff changeset
   315
*}
02b14a21761a Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 236
diff changeset
   316
02b14a21761a Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 236
diff changeset
   317
ML {*
02b14a21761a Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 236
diff changeset
   318
fun lookup_quot_thms lthy qty_name =
02b14a21761a Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 236
diff changeset
   319
  let
02b14a21761a Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 236
diff changeset
   320
    val thy = ProofContext.theory_of lthy;
02b14a21761a Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 236
diff changeset
   321
    val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2")
02b14a21761a Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 236
diff changeset
   322
    val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same")
269
fe6eb116b341 applic_prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 267
diff changeset
   323
    val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10")
529
6348c2a57ec2 More name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 527
diff changeset
   324
    val quot = PureThy.get_thm thy ("Quotient_" ^ qty_name)
239
02b14a21761a Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 236
diff changeset
   325
  in
269
fe6eb116b341 applic_prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 267
diff changeset
   326
    (trans2, reps_same, absrep, quot)
239
02b14a21761a Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 236
diff changeset
   327
  end
02b14a21761a Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 236
diff changeset
   328
*}
02b14a21761a Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 236
diff changeset
   329
402
dd64cca9265c recommited changes of comments
Christian Urban <urbanc@in.tum.de>
parents: 401
diff changeset
   330
section {* Regularization *} 
320
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   331
383
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
   332
(*
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
   333
Regularizing an rtrm means:
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
   334
 - quantifiers over a type that needs lifting are replaced by
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
   335
   bounded quantifiers, for example:
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
   336
      \<forall>x. P     \<Longrightarrow>     \<forall>x \<in> (Respects R). P  /  All (Respects R) P
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
   337
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
   338
   the relation R is given by the rty and qty;
330
1a0f0b758071 a little tuning of comments
Christian Urban <urbanc@in.tum.de>
parents: 326
diff changeset
   339
 
383
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
   340
 - abstractions over a type that needs lifting are replaced
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
   341
   by bounded abstractions:
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
   342
      \<lambda>x. P     \<Longrightarrow>     Ball (Respects R) (\<lambda>x. P)
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
   343
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
   344
 - equalities over the type being lifted are replaced by
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
   345
   corresponding relations:
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
   346
      A = B     \<Longrightarrow>     A \<approx> B
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
   347
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
   348
   example with more complicated types of A, B:
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
   349
      A = B     \<Longrightarrow>     (op = \<Longrightarrow> op \<approx>) A B
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
   350
*)
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
   351
404
d676974e3c89 more tuning
Christian Urban <urbanc@in.tum.de>
parents: 403
diff changeset
   352
ML {*
383
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
   353
(* builds the relation that is the argument of respects *)
320
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   354
fun mk_resp_arg lthy (rty, qty) =
319
0ae9d9e66cb7 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 316
diff changeset
   355
let
0ae9d9e66cb7 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 316
diff changeset
   356
  val thy = ProofContext.theory_of lthy
320
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   357
in  
334
5a7024be9083 code review with Cezary
Christian Urban <urbanc@in.tum.de>
parents: 330
diff changeset
   358
  if rty = qty
5a7024be9083 code review with Cezary
Christian Urban <urbanc@in.tum.de>
parents: 330
diff changeset
   359
  then HOLogic.eq_const rty
5a7024be9083 code review with Cezary
Christian Urban <urbanc@in.tum.de>
parents: 330
diff changeset
   360
  else
5a7024be9083 code review with Cezary
Christian Urban <urbanc@in.tum.de>
parents: 330
diff changeset
   361
    case (rty, qty) of
5a7024be9083 code review with Cezary
Christian Urban <urbanc@in.tum.de>
parents: 330
diff changeset
   362
      (Type (s, tys), Type (s', tys')) =>
320
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   363
       if s = s' 
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   364
       then let
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   365
              val SOME map_info = maps_lookup thy s
321
f46dc0ca08c3 simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
parents: 320
diff changeset
   366
              val args = map (mk_resp_arg lthy) (tys ~~ tys')
320
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   367
            in
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   368
              list_comb (Const (#relfun map_info, dummyT), args) 
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   369
            end  
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   370
       else let  
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   371
              val SOME qinfo = quotdata_lookup_thy thy s'
330
1a0f0b758071 a little tuning of comments
Christian Urban <urbanc@in.tum.de>
parents: 326
diff changeset
   372
              (* FIXME: check in this case that the rty and qty *)
1a0f0b758071 a little tuning of comments
Christian Urban <urbanc@in.tum.de>
parents: 326
diff changeset
   373
              (* FIXME: correspond to each other *)
353
9a0e8ab42ee8 fixed the error by a temporary fix (the data of the eqivalence relation should be only its name)
Christian Urban <urbanc@in.tum.de>
parents: 351
diff changeset
   374
              val (s, _) = dest_Const (#rel qinfo)
407
d387743f022b tuned comments and moved slightly some code
Christian Urban <urbanc@in.tum.de>
parents: 405
diff changeset
   375
              (* FIXME: the relation should only be the string        *)
d387743f022b tuned comments and moved slightly some code
Christian Urban <urbanc@in.tum.de>
parents: 405
diff changeset
   376
              (* FIXME: and the type needs to be calculated as below; *)
d387743f022b tuned comments and moved slightly some code
Christian Urban <urbanc@in.tum.de>
parents: 405
diff changeset
   377
              (* FIXME: maybe one should actually have a term         *)
d387743f022b tuned comments and moved slightly some code
Christian Urban <urbanc@in.tum.de>
parents: 405
diff changeset
   378
              (* FIXME: and one needs to force it to have this type   *)
320
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   379
            in
353
9a0e8ab42ee8 fixed the error by a temporary fix (the data of the eqivalence relation should be only its name)
Christian Urban <urbanc@in.tum.de>
parents: 351
diff changeset
   380
              Const (s, rty --> rty --> @{typ bool})
320
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   381
            end
334
5a7024be9083 code review with Cezary
Christian Urban <urbanc@in.tum.de>
parents: 330
diff changeset
   382
      | _ => HOLogic.eq_const dummyT 
351
3aba0cf85f97 tuned some comments
Christian Urban <urbanc@in.tum.de>
parents: 349
diff changeset
   383
             (* FIXME: check that the types correspond to each other? *)
320
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   384
end
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   385
*}
239
02b14a21761a Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 236
diff changeset
   386
320
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   387
ML {*
467
5ca4a927d7f0 more cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   388
val mk_babs = Const (@{const_name Babs}, dummyT)
5ca4a927d7f0 more cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   389
val mk_ball = Const (@{const_name Ball}, dummyT)
5ca4a927d7f0 more cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   390
val mk_bex  = Const (@{const_name Bex}, dummyT)
320
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   391
val mk_resp = Const (@{const_name Respects}, dummyT)
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   392
*}
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   393
323
Christian Urban <urbanc@in.tum.de>
parents: 321
diff changeset
   394
ML {*
330
1a0f0b758071 a little tuning of comments
Christian Urban <urbanc@in.tum.de>
parents: 326
diff changeset
   395
(* - applies f to the subterm of an abstraction,   *)
1a0f0b758071 a little tuning of comments
Christian Urban <urbanc@in.tum.de>
parents: 326
diff changeset
   396
(*   otherwise to the given term,                  *)
405
8bc7428745ad renamed REGULARIZE to be regularize
Christian Urban <urbanc@in.tum.de>
parents: 404
diff changeset
   397
(* - used by regularize, therefore abstracted      *)
330
1a0f0b758071 a little tuning of comments
Christian Urban <urbanc@in.tum.de>
parents: 326
diff changeset
   398
(*   variables do not have to be treated specially *)
1a0f0b758071 a little tuning of comments
Christian Urban <urbanc@in.tum.de>
parents: 326
diff changeset
   399
320
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   400
fun apply_subt f trm1 trm2 =
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   401
  case (trm1, trm2) of
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   402
    (Abs (x, T, t), Abs (x', T', t')) => Abs (x, T, f t t')
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   403
  | _ => f trm1 trm2
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   404
330
1a0f0b758071 a little tuning of comments
Christian Urban <urbanc@in.tum.de>
parents: 326
diff changeset
   405
(* the major type of All and Ex quantifiers *)
334
5a7024be9083 code review with Cezary
Christian Urban <urbanc@in.tum.de>
parents: 330
diff changeset
   406
fun qnt_typ ty = domain_type (domain_type ty)  
320
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   407
*}
319
0ae9d9e66cb7 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 316
diff changeset
   408
320
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   409
ML {*
330
1a0f0b758071 a little tuning of comments
Christian Urban <urbanc@in.tum.de>
parents: 326
diff changeset
   410
(* produces a regularized version of rtm      *)
1a0f0b758071 a little tuning of comments
Christian Urban <urbanc@in.tum.de>
parents: 326
diff changeset
   411
(* - the result is still not completely typed *)
1a0f0b758071 a little tuning of comments
Christian Urban <urbanc@in.tum.de>
parents: 326
diff changeset
   412
(* - does not need any special treatment of   *)
1a0f0b758071 a little tuning of comments
Christian Urban <urbanc@in.tum.de>
parents: 326
diff changeset
   413
(*   bound variables                          *)
1a0f0b758071 a little tuning of comments
Christian Urban <urbanc@in.tum.de>
parents: 326
diff changeset
   414
405
8bc7428745ad renamed REGULARIZE to be regularize
Christian Urban <urbanc@in.tum.de>
parents: 404
diff changeset
   415
fun regularize_trm lthy rtrm qtrm =
320
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   416
  case (rtrm, qtrm) of
325
Christian Urban <urbanc@in.tum.de>
parents: 323
diff changeset
   417
    (Abs (x, ty, t), Abs (x', ty', t')) =>
320
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   418
       let
405
8bc7428745ad renamed REGULARIZE to be regularize
Christian Urban <urbanc@in.tum.de>
parents: 404
diff changeset
   419
         val subtrm = regularize_trm lthy t t'
320
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   420
       in     
325
Christian Urban <urbanc@in.tum.de>
parents: 323
diff changeset
   421
         if ty = ty'
Christian Urban <urbanc@in.tum.de>
parents: 323
diff changeset
   422
         then Abs (x, ty, subtrm)
326
e755a5da14c8 my first version of repabs injection
Christian Urban <urbanc@in.tum.de>
parents: 325
diff changeset
   423
         else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm
320
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   424
       end
549
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   425
320
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   426
  | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   427
       let
405
8bc7428745ad renamed REGULARIZE to be regularize
Christian Urban <urbanc@in.tum.de>
parents: 404
diff changeset
   428
         val subtrm = apply_subt (regularize_trm lthy) t t'
320
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   429
       in
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   430
         if ty = ty'
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   431
         then Const (@{const_name "All"}, ty) $ subtrm
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   432
         else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   433
       end
549
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   434
320
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   435
  | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   436
       let
405
8bc7428745ad renamed REGULARIZE to be regularize
Christian Urban <urbanc@in.tum.de>
parents: 404
diff changeset
   437
         val subtrm = apply_subt (regularize_trm lthy) t t'
320
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   438
       in
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   439
         if ty = ty'
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   440
         then Const (@{const_name "Ex"}, ty) $ subtrm
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   441
         else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   442
       end
549
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   443
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   444
  | (* equalities need to be replaced by appropriate equivalence relations *) 
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   445
    (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   446
         if ty = ty'
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   447
         then rtrm
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   448
         else mk_resp_arg lthy (domain_type ty, domain_type ty') 
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   449
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   450
  | (* in this case we check whether the given equivalence relation is correct *) 
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   451
    (rel, Const (@{const_name "op ="}, ty')) =>
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   452
       let 
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   453
         val exc = LIFT_MATCH "regularise (relation mismatch)"
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   454
         val rel_ty = (fastype_of rel) handle TERM _ => raise exc 
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   455
         val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') 
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   456
       in 
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   457
         if rel' = rel
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   458
         then rtrm
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   459
         else raise exc
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   460
       end  
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   461
  | (_, Const (s, _)) =>
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   462
       let 
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   463
         fun same_name (Const (s, _)) (Const (s', _)) = (s = s')
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   464
           | same_name _ _ = false
320
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   465
       in
549
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   466
         if same_name rtrm qtrm 
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   467
         then rtrm 
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   468
         else 
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   469
           let 
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   470
             fun exc1 s = LIFT_MATCH ("regularize (constant " ^ s ^ " not found)")
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   471
             val exc2   = LIFT_MATCH ("regularize (constant mismatch)")
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   472
             val thy = ProofContext.theory_of lthy
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   473
             val rtrm' = (#rconst (qconsts_lookup thy s)) handle NotFound => raise (exc1 s) 
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   474
           in 
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   475
             if matches_term (rtrm, rtrm')
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   476
             then rtrm
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   477
             else raise exc2
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   478
           end
320
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   479
       end 
549
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   480
320
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   481
  | (t1 $ t2, t1' $ t2') =>
405
8bc7428745ad renamed REGULARIZE to be regularize
Christian Urban <urbanc@in.tum.de>
parents: 404
diff changeset
   482
       (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2')
549
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   483
453
c22ab554a32d started functions for qid-insertion and fixed a bug in regularise
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   484
  | (Free (x, ty), Free (x', ty')) => 
c22ab554a32d started functions for qid-insertion and fixed a bug in regularise
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   485
       (* this case cannot arrise as we start with two fully atomized terms *)
c22ab554a32d started functions for qid-insertion and fixed a bug in regularise
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   486
       raise (LIFT_MATCH "regularize (frees)")
549
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   487
320
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   488
  | (Bound i, Bound i') =>
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   489
       if i = i' 
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   490
       then rtrm 
549
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   491
       else raise (LIFT_MATCH "regularize (bounds mismatch)")
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   492
f178958d3d81 not yet quite functional treatment of constants
Christian Urban <urbanc@in.tum.de>
parents: 544
diff changeset
   493
  | (rt, qt) =>
374
980fdf92a834 fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents: 372
diff changeset
   494
       raise (LIFT_MATCH "regularize (default)")
320
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   495
*}
7d3d86beacd6 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents: 319
diff changeset
   496
321
f46dc0ca08c3 simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
parents: 320
diff changeset
   497
(*
407
d387743f022b tuned comments and moved slightly some code
Christian Urban <urbanc@in.tum.de>
parents: 405
diff changeset
   498
FIXME / TODO: needs to be adapted
d387743f022b tuned comments and moved slightly some code
Christian Urban <urbanc@in.tum.de>
parents: 405
diff changeset
   499
383
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
   500
To prove that the raw theorem implies the regularised one, 
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
   501
we try in order:
330
1a0f0b758071 a little tuning of comments
Christian Urban <urbanc@in.tum.de>
parents: 326
diff changeset
   502
321
f46dc0ca08c3 simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
parents: 320
diff changeset
   503
 - Reflexivity of the relation
f46dc0ca08c3 simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
parents: 320
diff changeset
   504
 - Assumption
f46dc0ca08c3 simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
parents: 320
diff changeset
   505
 - Elimnating quantifiers on both sides of toplevel implication
f46dc0ca08c3 simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
parents: 320
diff changeset
   506
 - Simplifying implications on both sides of toplevel implication
f46dc0ca08c3 simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
parents: 320
diff changeset
   507
 - Ball (Respects ?E) ?P = All ?P
f46dc0ca08c3 simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
parents: 320
diff changeset
   508
 - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
f46dc0ca08c3 simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
parents: 320
diff changeset
   509
f46dc0ca08c3 simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
parents: 320
diff changeset
   510
*)
f46dc0ca08c3 simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
parents: 320
diff changeset
   511
400
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 398
diff changeset
   512
ML {*
582
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   513
fun equiv_tac ctxt =
420
dcfe009c98aa replaced FIRST' (map rtac list) with resolve_tac list
Christian Urban <urbanc@in.tum.de>
parents: 419
diff changeset
   514
  REPEAT_ALL_NEW (FIRST' 
582
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   515
    [resolve_tac (equiv_rules_get ctxt)])
400
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 398
diff changeset
   516
*}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 398
diff changeset
   517
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 398
diff changeset
   518
ML {*
583
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   519
fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   520
val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   521
*}
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   522
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   523
ML {*
582
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   524
fun ball_reg_eqv_simproc ss redex =
432
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   525
  let
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   526
    val ctxt = Simplifier.the_context ss
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   527
    val thy = ProofContext.theory_of ctxt
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   528
  in
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   529
  case redex of
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   530
      (ogl as ((Const (@{const_name "Ball"}, _)) $
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   531
        ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   532
      (let
529
6348c2a57ec2 More name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 527
diff changeset
   533
        val gl = Const (@{const_name "equivp"}, dummyT) $ R;
432
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   534
        val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
582
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   535
        val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 1)
432
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   536
        val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv} OF [eqv]]);
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   537
(*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *)
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   538
      in
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   539
        SOME thm
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   540
      end
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   541
      handle _ => NONE
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   542
      )
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   543
  | _ => NONE
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   544
  end
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   545
*}
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   546
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   547
ML {*
582
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   548
fun bex_reg_eqv_simproc ss redex =
432
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   549
  let
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   550
    val ctxt = Simplifier.the_context ss
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   551
    val thy = ProofContext.theory_of ctxt
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   552
  in
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   553
  case redex of
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   554
      (ogl as ((Const (@{const_name "Bex"}, _)) $
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   555
        ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   556
      (let
529
6348c2a57ec2 More name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 527
diff changeset
   557
        val gl = Const (@{const_name "equivp"}, dummyT) $ R;
432
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   558
        val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
582
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   559
        val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 1)
432
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   560
        val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv} OF [eqv]]);
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   561
(*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *)
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   562
      in
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   563
        SOME thm
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   564
      end
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   565
      handle _ => NONE
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   566
      )
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   567
  | _ => NONE
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   568
  end
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   569
*}
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   570
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   571
ML {*
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   572
fun prep_trm thy (x, (T, t)) =
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   573
  (cterm_of thy (Var (x, T)), cterm_of thy t)
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   574
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   575
fun prep_ty thy (x, (S, ty)) =
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   576
  (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   577
*}
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   578
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   579
ML {*
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   580
fun matching_prs thy pat trm =
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   581
let
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   582
  val univ = Unify.matchers thy [(pat, trm)]
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   583
  val SOME (env, _) = Seq.pull univ
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   584
  val tenv = Vartab.dest (Envir.term_env env)
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   585
  val tyenv = Vartab.dest (Envir.type_env env)
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   586
in
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   587
  (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   588
end
400
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 398
diff changeset
   589
*}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 398
diff changeset
   590
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 398
diff changeset
   591
ML {*
582
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   592
fun ball_reg_eqv_range_simproc ss redex =
400
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 398
diff changeset
   593
  let
432
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   594
    val ctxt = Simplifier.the_context ss
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   595
    val thy = ProofContext.theory_of ctxt
400
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 398
diff changeset
   596
  in
432
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   597
  case redex of
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   598
      (ogl as ((Const (@{const_name "Ball"}, _)) $
536
44fa9df44e6f More code cleaning and name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 529
diff changeset
   599
        ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "fun_rel"}, _)) $ R1 $ R2)) $ _)) =>
432
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   600
      (let
529
6348c2a57ec2 More name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 527
diff changeset
   601
        val gl = Const (@{const_name "equivp"}, dummyT) $ R2;
432
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   602
        val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
487
f5db9ede89b0 Experiments with OPTION_map
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 486
diff changeset
   603
(*        val _ = tracing (Syntax.string_of_term ctxt glc);*)
582
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   604
        val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 1)
432
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   605
        val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv_range} OF [eqv]]);
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   606
        val R1c = cterm_of thy R1;
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   607
        val thmi = Drule.instantiate' [] [SOME R1c] thm;
487
f5db9ede89b0 Experiments with OPTION_map
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 486
diff changeset
   608
(*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi));*)
432
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   609
        val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   610
        val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);
487
f5db9ede89b0 Experiments with OPTION_map
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 486
diff changeset
   611
(*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2)); *)
432
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   612
      in
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   613
        SOME thm2
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   614
      end
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   615
      handle _ => NONE
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   616
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   617
      )
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   618
  | _ => NONE
400
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 398
diff changeset
   619
  end
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 398
diff changeset
   620
*}
432
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   621
583
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   622
578
070161f1996a updated Isabelle and deleted mono rules
Christian Urban <urbanc@in.tum.de>
parents: 577
diff changeset
   623
thm bex_reg_eqv_range
583
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   624
thm ball_reg_eqv
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   625
thm bex_reg_eqv
578
070161f1996a updated Isabelle and deleted mono rules
Christian Urban <urbanc@in.tum.de>
parents: 577
diff changeset
   626
432
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   627
ML {*
582
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   628
fun bex_reg_eqv_range_simproc ss redex =
432
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   629
  let
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   630
    val ctxt = Simplifier.the_context ss
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   631
    val thy = ProofContext.theory_of ctxt
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   632
  in
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   633
  case redex of
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   634
      (ogl as ((Const (@{const_name "Bex"}, _)) $
536
44fa9df44e6f More code cleaning and name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 529
diff changeset
   635
        ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "fun_rel"}, _)) $ R1 $ R2)) $ _)) =>
432
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   636
      (let
529
6348c2a57ec2 More name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 527
diff changeset
   637
        val gl = Const (@{const_name "equivp"}, dummyT) $ R2;
432
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   638
        val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
487
f5db9ede89b0 Experiments with OPTION_map
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 486
diff changeset
   639
(*        val _ = tracing (Syntax.string_of_term ctxt glc); *)
582
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   640
        val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 1)
432
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   641
        val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv_range} OF [eqv]]);
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   642
        val R1c = cterm_of thy R1;
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   643
        val thmi = Drule.instantiate' [] [SOME R1c] thm;
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   644
(*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *)
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   645
        val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   646
        val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);
487
f5db9ede89b0 Experiments with OPTION_map
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 486
diff changeset
   647
(*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2));*)
432
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   648
      in
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   649
        SOME thm2
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   650
      end
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   651
      handle _ => NONE
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   652
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   653
      )
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   654
  | _ => NONE
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   655
  end
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   656
*}
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   657
529
6348c2a57ec2 More name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 527
diff changeset
   658
lemma eq_imp_rel: "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
6348c2a57ec2 More name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 527
diff changeset
   659
by (simp add: equivp_reflp)
432
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   660
583
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   661
(* does not work yet
432
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   662
ML {*
582
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   663
fun regularize_tac ctxt =
432
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   664
  let
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   665
    val pat1 = [@{term "Ball (Respects R) P"}];
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   666
    val pat2 = [@{term "Bex (Respects R) P"}];
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   667
    val pat3 = [@{term "Ball (Respects (R1 ===> R2)) P"}];
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   668
    val pat4 = [@{term "Bex (Respects (R1 ===> R2)) P"}];
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   669
    val thy = ProofContext.theory_of ctxt
582
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   670
    val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc))
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   671
    val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc))
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   672
    val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc))
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   673
    val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc))
583
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   674
    val simp_set = HOL_basic_ss addsimps @{thms ball_reg_eqv bex_reg_eqv}
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   675
                                 addsimprocs [simproc3, simproc4]
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   676
                                 addSolver equiv_solver
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   677
    * TODO: Make sure that there are no list_rel, pair_rel etc involved *
582
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
   678
    val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt)
432
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   679
  in
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   680
  ObjectLogic.full_atomize_tac THEN'
583
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   681
  simp_tac simp_set THEN'
432
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   682
  REPEAT_ALL_NEW (FIRST' [
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   683
    rtac @{thm ball_reg_right},
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   684
    rtac @{thm bex_reg_left},
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   685
    resolve_tac (Inductive.get_monos ctxt),
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   686
    rtac @{thm ball_all_comm},
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   687
    rtac @{thm bex_ex_comm},
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   688
    resolve_tac eq_eqvs,
583
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   689
    simp_tac simp_set
432
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   690
  ])
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   691
  end
583
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   692
*}*)
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   693
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   694
ML {*
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   695
fun regularize_tac ctxt =
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   696
let
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   697
  val pat1 = [@{term "Ball (Respects R) P"}];
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   698
  val pat2 = [@{term "Bex (Respects R) P"}];
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   699
  val pat3 = [@{term "Ball (Respects (R1 ===> R2)) P"}];
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   700
  val pat4 = [@{term "Bex (Respects (R1 ===> R2)) P"}];
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   701
  val thy = ProofContext.theory_of ctxt
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   702
  val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc))
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   703
  val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc))
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   704
  val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc))
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   705
  val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc))
588
2c95d0436a2b removed usage of HOL_basic_ss by using a slighly extended version of empty_ss
Christian Urban <urbanc@in.tum.de>
parents: 586
diff changeset
   706
  val simp_ctxt = (mk_minimal_ss ctxt) addsimprocs [simproc1, simproc2, simproc3, simproc4] 
583
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   707
  (* TODO: Make sure that there are no list_rel, pair_rel etc involved *)
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   708
  val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt)
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   709
in
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   710
  ObjectLogic.full_atomize_tac THEN'
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   711
  simp_tac simp_ctxt THEN'
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   712
  REPEAT_ALL_NEW (FIRST' [
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   713
     rtac @{thm ball_reg_right},
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   714
     rtac @{thm bex_reg_left},
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   715
     resolve_tac (Inductive.get_monos ctxt),
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   716
     rtac @{thm ball_all_comm},
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   717
     rtac @{thm bex_ex_comm},
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   718
     resolve_tac eq_eqvs,
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   719
     simp_tac simp_ctxt])
7414f6cb5398 working state again
Christian Urban <urbanc@in.tum.de>
parents: 582
diff changeset
   720
end
432
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 427
diff changeset
   721
*}
390
1dd6a21cdd1c test with monos
Christian Urban <urbanc@in.tum.de>
parents: 388
diff changeset
   722
544
c15eea8d20af Minor renames and moving
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 543
diff changeset
   723
section {* Injections of rep and abses *}
383
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
   724
381
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   725
(*
544
c15eea8d20af Minor renames and moving
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 543
diff changeset
   726
Injecting repabs means:
381
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   727
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   728
  For abstractions:
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   729
  * If the type of the abstraction doesn't need lifting we recurse.
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   730
  * If it does we add RepAbs around the whole term and check if the
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   731
    variable needs lifting.
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   732
    * If it doesn't then we recurse
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   733
    * If it does we recurse and put 'RepAbs' around all occurences
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   734
      of the variable in the obtained subterm. This in combination
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   735
      with the RepAbs above will let us change the type of the
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   736
      abstraction with rewriting.
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   737
  For applications:
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   738
  * If the term is 'Respects' applied to anything we leave it unchanged
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   739
  * If the term needs lifting and the head is a constant that we know
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   740
    how to lift, we put a RepAbs and recurse
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   741
  * If the term needs lifting and the head is a free applied to subterms
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   742
    (if it is not applied we treated it in Abs branch) then we
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   743
    put RepAbs and recurse
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   744
  * Otherwise just recurse.
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   745
*)
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
   746
336
e6b6e5ba0cc5 Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 334
diff changeset
   747
ML {*
e6b6e5ba0cc5 Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 334
diff changeset
   748
fun mk_repabs lthy (T, T') trm = 
e6b6e5ba0cc5 Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 334
diff changeset
   749
  Quotient_Def.get_fun repF lthy (T, T') 
354
2eb6d527dfe4 addded a tactic, which sets up the three goals of the `algorithm'
Christian Urban <urbanc@in.tum.de>
parents: 353
diff changeset
   750
    $ (Quotient_Def.get_fun absF lthy (T, T') $ trm)
336
e6b6e5ba0cc5 Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 334
diff changeset
   751
*}
e6b6e5ba0cc5 Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 334
diff changeset
   752
e6b6e5ba0cc5 Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 334
diff changeset
   753
ML {*
563
ff37ffbb128a further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 562
diff changeset
   754
(* bound variables need to be treated properly,    *)
ff37ffbb128a further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 562
diff changeset
   755
(* as the type of subterms need to be calculated   *)
ff37ffbb128a further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 562
diff changeset
   756
(* in the abstraction case                         *)
336
e6b6e5ba0cc5 Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 334
diff changeset
   757
408
1056861b562c renamed inj_REPABS to inj_repabs_trm
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   758
fun inj_repabs_trm lthy (rtrm, qtrm) =
563
ff37ffbb128a further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 562
diff changeset
   759
 case (rtrm, qtrm) of
336
e6b6e5ba0cc5 Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 334
diff changeset
   760
    (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
408
1056861b562c renamed inj_REPABS to inj_repabs_trm
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   761
       Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
552
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
parents: 551
diff changeset
   762
336
e6b6e5ba0cc5 Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 334
diff changeset
   763
  | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
408
1056861b562c renamed inj_REPABS to inj_repabs_trm
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   764
       Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
552
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
parents: 551
diff changeset
   765
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
parents: 551
diff changeset
   766
  | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) =>
408
1056861b562c renamed inj_REPABS to inj_repabs_trm
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   767
       Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
552
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
parents: 551
diff changeset
   768
336
e6b6e5ba0cc5 Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 334
diff changeset
   769
  | (Abs (x, T, t), Abs (x', T', t')) =>
e6b6e5ba0cc5 Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 334
diff changeset
   770
      let
563
ff37ffbb128a further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 562
diff changeset
   771
        val rty = fastype_of rtrm
ff37ffbb128a further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 562
diff changeset
   772
        val qty = fastype_of qtrm
336
e6b6e5ba0cc5 Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 334
diff changeset
   773
        val (y, s) = Term.dest_abs (x, T, t)
e6b6e5ba0cc5 Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 334
diff changeset
   774
        val (_, s') = Term.dest_abs (x', T', t')
e6b6e5ba0cc5 Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 334
diff changeset
   775
        val yvar = Free (y, T)
453
c22ab554a32d started functions for qid-insertion and fixed a bug in regularise
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   776
        val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s'))
336
e6b6e5ba0cc5 Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 334
diff changeset
   777
      in
345
573e2b625e8e a version of inj_REPABS (needs to be looked at again later)
Christian Urban <urbanc@in.tum.de>
parents: 341
diff changeset
   778
        if rty = qty 
573e2b625e8e a version of inj_REPABS (needs to be looked at again later)
Christian Urban <urbanc@in.tum.de>
parents: 341
diff changeset
   779
        then result
573e2b625e8e a version of inj_REPABS (needs to be looked at again later)
Christian Urban <urbanc@in.tum.de>
parents: 341
diff changeset
   780
        else mk_repabs lthy (rty, qty) result
336
e6b6e5ba0cc5 Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 334
diff changeset
   781
      end
560
d707839bd917 simplified inj_repabs_trm
Christian Urban <urbanc@in.tum.de>
parents: 559
diff changeset
   782
d707839bd917 simplified inj_repabs_trm
Christian Urban <urbanc@in.tum.de>
parents: 559
diff changeset
   783
  | (t $ s, t' $ s') =>  
d707839bd917 simplified inj_repabs_trm
Christian Urban <urbanc@in.tum.de>
parents: 559
diff changeset
   784
       (inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s'))
d707839bd917 simplified inj_repabs_trm
Christian Urban <urbanc@in.tum.de>
parents: 559
diff changeset
   785
563
ff37ffbb128a further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 562
diff changeset
   786
  | (Free (_, T), Free (_, T')) => 
560
d707839bd917 simplified inj_repabs_trm
Christian Urban <urbanc@in.tum.de>
parents: 559
diff changeset
   787
        if T = T' 
d707839bd917 simplified inj_repabs_trm
Christian Urban <urbanc@in.tum.de>
parents: 559
diff changeset
   788
        then rtrm 
d707839bd917 simplified inj_repabs_trm
Christian Urban <urbanc@in.tum.de>
parents: 559
diff changeset
   789
        else mk_repabs lthy (T, T') rtrm
d707839bd917 simplified inj_repabs_trm
Christian Urban <urbanc@in.tum.de>
parents: 559
diff changeset
   790
568
0384e039b7f2 added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   791
  | (_, Const (@{const_name "op ="}, _)) => rtrm
0384e039b7f2 added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   792
576
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   793
    (* FIXME: check here that rtrm is the corresponding definition for the const *)
568
0384e039b7f2 added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   794
  | (_, Const (_, T')) =>
0384e039b7f2 added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   795
      let
0384e039b7f2 added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   796
        val rty = fastype_of rtrm
0384e039b7f2 added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   797
      in 
0384e039b7f2 added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   798
        if rty = T'                    
560
d707839bd917 simplified inj_repabs_trm
Christian Urban <urbanc@in.tum.de>
parents: 559
diff changeset
   799
        then rtrm
568
0384e039b7f2 added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   800
        else mk_repabs lthy (rty, T') rtrm
0384e039b7f2 added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   801
      end   
560
d707839bd917 simplified inj_repabs_trm
Christian Urban <urbanc@in.tum.de>
parents: 559
diff changeset
   802
  
d707839bd917 simplified inj_repabs_trm
Christian Urban <urbanc@in.tum.de>
parents: 559
diff changeset
   803
  | _ => raise (LIFT_MATCH "injection")
336
e6b6e5ba0cc5 Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 334
diff changeset
   804
*}
e6b6e5ba0cc5 Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 334
diff changeset
   805
404
d676974e3c89 more tuning
Christian Urban <urbanc@in.tum.de>
parents: 403
diff changeset
   806
section {* RepAbs Injection Tactic *}
387
f78aa16daae5 reordered the code
Christian Urban <urbanc@in.tum.de>
parents: 386
diff changeset
   807
f78aa16daae5 reordered the code
Christian Urban <urbanc@in.tum.de>
parents: 386
diff changeset
   808
ML {*
506
91c374abde06 removed quot argument...not all examples work anymore
Christian Urban <urbanc@in.tum.de>
parents: 505
diff changeset
   809
fun quotient_tac ctxt =
468
10d75457792f Removed last HOL_ss
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 467
diff changeset
   810
  REPEAT_ALL_NEW (FIRST'
542
fe468f8723fc More cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 541
diff changeset
   811
    [rtac @{thm identity_quotient},
510
8dbc521ee97f Even better: Completely got rid of the simps in both quotient_tac and inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 509
diff changeset
   812
     resolve_tac (quotient_rules_get ctxt)])
387
f78aa16daae5 reordered the code
Christian Urban <urbanc@in.tum.de>
parents: 386
diff changeset
   813
*}
f78aa16daae5 reordered the code
Christian Urban <urbanc@in.tum.de>
parents: 386
diff changeset
   814
568
0384e039b7f2 added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   815
(* solver for the simplifier *)
0384e039b7f2 added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   816
ML {*
0384e039b7f2 added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   817
fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
0384e039b7f2 added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   818
val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
0384e039b7f2 added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   819
*}
0384e039b7f2 added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents: 564
diff changeset
   820
576
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   821
ML {*
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   822
fun solve_quotient_assums ctxt thm =
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   823
  let val gl = hd (Drule.strip_imp_prems (cprop_of thm)) in
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   824
  thm OF [Goal.prove_internal [] gl (fn _ => quotient_tac ctxt 1)]
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   825
  end
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   826
  handle _ => error "solve_quotient_assums"
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   827
*}
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   828
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   829
(* It proves the Quotient assumptions by calling quotient_tac *)
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   830
ML {*
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   831
fun solve_quotient_assum i ctxt thm =
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   832
  let
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   833
    val tac =
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   834
      (compose_tac (false, thm, i)) THEN_ALL_NEW
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   835
      (quotient_tac ctxt);
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   836
    val gc = Drule.strip_imp_concl (cprop_of thm);
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   837
  in
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   838
    Goal.prove_internal [] gc (fn _ => tac 1)
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   839
  end
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   840
  handle _ => error "solve_quotient_assum"
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   841
*}
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   842
480
7fbbb2690bc5 Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 479
diff changeset
   843
definition
7fbbb2690bc5 Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 479
diff changeset
   844
  "QUOT_TRUE x \<equiv> True"
472
cb03d4b3f059 fixed problems with FOCUS
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
   845
387
f78aa16daae5 reordered the code
Christian Urban <urbanc@in.tum.de>
parents: 386
diff changeset
   846
ML {*
480
7fbbb2690bc5 Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 479
diff changeset
   847
fun find_qt_asm asms =
7fbbb2690bc5 Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 479
diff changeset
   848
  let
7fbbb2690bc5 Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 479
diff changeset
   849
    fun find_fun trm =
7fbbb2690bc5 Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 479
diff changeset
   850
      case trm of
7fbbb2690bc5 Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 479
diff changeset
   851
        (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true
7fbbb2690bc5 Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 479
diff changeset
   852
      | _ => false
7fbbb2690bc5 Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 479
diff changeset
   853
  in
7fbbb2690bc5 Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 479
diff changeset
   854
    case find_first find_fun asms of
7fbbb2690bc5 Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 479
diff changeset
   855
      SOME (_ $ (_ $ (f $ a))) => (f, a)
575
334b3e9ea3e0 Handle 'find_qt_asm' exception. Now all inj_repabs_goals should be solved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 572
diff changeset
   856
    | SOME _ => error "find_qt_asm: no pair"
334b3e9ea3e0 Handle 'find_qt_asm' exception. Now all inj_repabs_goals should be solved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 572
diff changeset
   857
    | NONE => error "find_qt_asm: no assumption"
480
7fbbb2690bc5 Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 479
diff changeset
   858
  end
7fbbb2690bc5 Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 479
diff changeset
   859
*}
7fbbb2690bc5 Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 479
diff changeset
   860
398
fafcc54e531d some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents: 391
diff changeset
   861
(*
fafcc54e531d some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents: 391
diff changeset
   862
To prove that the regularised theorem implies the abs/rep injected, 
fafcc54e531d some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents: 391
diff changeset
   863
we try:
fafcc54e531d some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents: 391
diff changeset
   864
fafcc54e531d some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents: 391
diff changeset
   865
 1) theorems 'trans2' from the appropriate QUOT_TYPE
476
325d6e9a7515 Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 475
diff changeset
   866
 2) remove lambdas from both sides: lambda_rsp_tac
398
fafcc54e531d some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents: 391
diff changeset
   867
 3) remove Ball/Bex from the right hand side
fafcc54e531d some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents: 391
diff changeset
   868
 4) use user-supplied RSP theorems
fafcc54e531d some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents: 391
diff changeset
   869
 5) remove rep_abs from the right side
fafcc54e531d some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents: 391
diff changeset
   870
 6) reflexivity of equality
fafcc54e531d some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents: 391
diff changeset
   871
 7) split applications of lifted type (apply_rsp)
fafcc54e531d some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents: 391
diff changeset
   872
 8) split applications of non-lifted type (cong_tac)
fafcc54e531d some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents: 391
diff changeset
   873
 9) apply extentionality
423
2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
parents: 420
diff changeset
   874
 A) reflexivity of the relation
2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
parents: 420
diff changeset
   875
 B) assumption
398
fafcc54e531d some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents: 391
diff changeset
   876
    (Lambdas under respects may have left us some assumptions)
423
2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
parents: 420
diff changeset
   877
 C) proving obvious higher order equalities by simplifying fun_rel
398
fafcc54e531d some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents: 391
diff changeset
   878
    (not sure if it is still needed?)
423
2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
parents: 420
diff changeset
   879
 D) unfolding lambda on one side
2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
parents: 420
diff changeset
   880
 E) simplifying (= ===> =) for simpler respectfulness
398
fafcc54e531d some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents: 391
diff changeset
   881
fafcc54e531d some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents: 391
diff changeset
   882
*)
fafcc54e531d some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents: 391
diff changeset
   883
469
6d077eac6ad7 QUOT_TRUE joke
Christian Urban <urbanc@in.tum.de>
parents: 468
diff changeset
   884
lemma quot_true_dests:
6d077eac6ad7 QUOT_TRUE joke
Christian Urban <urbanc@in.tum.de>
parents: 468
diff changeset
   885
  shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P"
476
325d6e9a7515 Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 475
diff changeset
   886
  and   QT_ex:  "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P"
469
6d077eac6ad7 QUOT_TRUE joke
Christian Urban <urbanc@in.tum.de>
parents: 468
diff changeset
   887
  and   QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE  (P x))"
476
325d6e9a7515 Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 475
diff changeset
   888
  and   QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)"
325d6e9a7515 Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 475
diff changeset
   889
apply(simp_all add: QUOT_TRUE_def ext)
469
6d077eac6ad7 QUOT_TRUE joke
Christian Urban <urbanc@in.tum.de>
parents: 468
diff changeset
   890
done
6d077eac6ad7 QUOT_TRUE joke
Christian Urban <urbanc@in.tum.de>
parents: 468
diff changeset
   891
476
325d6e9a7515 Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 475
diff changeset
   892
lemma QUOT_TRUE_i: "(QUOT_TRUE (a :: bool) \<Longrightarrow> P) \<Longrightarrow> P"
470
fc16faef5dfa Transformation of QUOT_TRUE assumption by any given function
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 469
diff changeset
   893
by (simp add: QUOT_TRUE_def)
fc16faef5dfa Transformation of QUOT_TRUE assumption by any given function
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 469
diff changeset
   894
479
24799397a3ce The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 476
diff changeset
   895
lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b"
470
fc16faef5dfa Transformation of QUOT_TRUE assumption by any given function
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 469
diff changeset
   896
by (simp add: QUOT_TRUE_def)
fc16faef5dfa Transformation of QUOT_TRUE assumption by any given function
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 469
diff changeset
   897
fc16faef5dfa Transformation of QUOT_TRUE assumption by any given function
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 469
diff changeset
   898
ML {*
479
24799397a3ce The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 476
diff changeset
   899
fun quot_true_conv1 ctxt fnctn ctrm =
24799397a3ce The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 476
diff changeset
   900
  case (term_of ctrm) of
24799397a3ce The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 476
diff changeset
   901
    (Const (@{const_name QUOT_TRUE}, _) $ x) =>
24799397a3ce The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 476
diff changeset
   902
    let
24799397a3ce The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 476
diff changeset
   903
      val fx = fnctn x;
24799397a3ce The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 476
diff changeset
   904
      val thy = ProofContext.theory_of ctxt;
24799397a3ce The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 476
diff changeset
   905
      val cx = cterm_of thy x;
24799397a3ce The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 476
diff changeset
   906
      val cfx = cterm_of thy fx;
24799397a3ce The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 476
diff changeset
   907
      val cxt = ctyp_of thy (fastype_of x);
24799397a3ce The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 476
diff changeset
   908
      val cfxt = ctyp_of thy (fastype_of fx);
24799397a3ce The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 476
diff changeset
   909
      val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QUOT_TRUE_imp}
24799397a3ce The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 476
diff changeset
   910
    in
24799397a3ce The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 476
diff changeset
   911
      Conv.rewr_conv thm ctrm
24799397a3ce The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 476
diff changeset
   912
    end
470
fc16faef5dfa Transformation of QUOT_TRUE assumption by any given function
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 469
diff changeset
   913
*}
469
6d077eac6ad7 QUOT_TRUE joke
Christian Urban <urbanc@in.tum.de>
parents: 468
diff changeset
   914
479
24799397a3ce The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 476
diff changeset
   915
ML {*
24799397a3ce The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 476
diff changeset
   916
fun quot_true_conv ctxt fnctn ctrm =
24799397a3ce The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 476
diff changeset
   917
  case (term_of ctrm) of
24799397a3ce The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 476
diff changeset
   918
    (Const (@{const_name QUOT_TRUE}, _) $ _) =>
24799397a3ce The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 476
diff changeset
   919
      quot_true_conv1 ctxt fnctn ctrm
24799397a3ce The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 476
diff changeset
   920
  | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm
24799397a3ce The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 476
diff changeset
   921
  | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
24799397a3ce The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 476
diff changeset
   922
  | _ => Conv.all_conv ctrm
24799397a3ce The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 476
diff changeset
   923
*}
24799397a3ce The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 476
diff changeset
   924
24799397a3ce The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 476
diff changeset
   925
ML {*
493
672b94510e7d deleted some dead code
Christian Urban <urbanc@in.tum.de>
parents: 492
diff changeset
   926
fun quot_true_tac ctxt fnctn = CONVERSION
672b94510e7d deleted some dead code
Christian Urban <urbanc@in.tum.de>
parents: 492
diff changeset
   927
    ((Conv.params_conv ~1 (fn ctxt =>
672b94510e7d deleted some dead code
Christian Urban <urbanc@in.tum.de>
parents: 492
diff changeset
   928
       (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)
479
24799397a3ce The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 476
diff changeset
   929
*}
476
325d6e9a7515 Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 475
diff changeset
   930
325d6e9a7515 Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 475
diff changeset
   931
ML {* fun dest_comb (f $ a) = (f, a) *}
325d6e9a7515 Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 475
diff changeset
   932
ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *}
481
7f97c52021c9 Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 480
diff changeset
   933
(* TODO: Can this be done easier? *)
7f97c52021c9 Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 480
diff changeset
   934
ML {*
7f97c52021c9 Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 480
diff changeset
   935
fun unlam t =
7f97c52021c9 Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 480
diff changeset
   936
  case t of
7f97c52021c9 Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 480
diff changeset
   937
    (Abs a) => snd (Term.dest_abs a)
525
3f657c4fbefa Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 523
diff changeset
   938
  | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))
398
fafcc54e531d some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents: 391
diff changeset
   939
*}
fafcc54e531d some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents: 391
diff changeset
   940
522
6b77cfd508e9 rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 519
diff changeset
   941
ML {*
6b77cfd508e9 rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 519
diff changeset
   942
fun dest_fun_type (Type("fun", [T, S])) = (T, S)
6b77cfd508e9 rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 519
diff changeset
   943
  | dest_fun_type _ = error "dest_fun_type"
6b77cfd508e9 rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 519
diff changeset
   944
*}
6b77cfd508e9 rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 519
diff changeset
   945
6b77cfd508e9 rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 519
diff changeset
   946
ML {*
551
34d12737b379 tuned code
Christian Urban <urbanc@in.tum.de>
parents: 550
diff changeset
   947
val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
34d12737b379 tuned code
Christian Urban <urbanc@in.tum.de>
parents: 550
diff changeset
   948
*}
34d12737b379 tuned code
Christian Urban <urbanc@in.tum.de>
parents: 550
diff changeset
   949
34d12737b379 tuned code
Christian Urban <urbanc@in.tum.de>
parents: 550
diff changeset
   950
ML {*
576
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   951
val apply_rsp_tac =
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   952
  Subgoal.FOCUS (fn {concl, asms, context,...} =>
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   953
    case ((HOLogic.dest_Trueprop (term_of concl))) of
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   954
      ((R2 $ (f $ x) $ (g $ y))) =>
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   955
        (let
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   956
          val (asmf, asma) = find_qt_asm (map term_of asms);
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   957
        in
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   958
          if (fastype_of asmf) = (fastype_of f) then no_tac else let
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   959
            val ty_a = fastype_of x;
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   960
            val ty_b = fastype_of asma;
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   961
            val ty_c = range_type (type_of f);
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   962
            val thy = ProofContext.theory_of context;
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   963
            val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c];
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   964
            val thm = Drule.instantiate' ty_inst [] @{thm apply_rsp}
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   965
            val te = solve_quotient_assums context thm
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   966
            val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   967
            val thm = Drule.instantiate' [] t_inst te
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   968
          in
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   969
            compose_tac (false, thm, 2) 1
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   970
          end
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   971
        end
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   972
        handle ERROR "find_qt_asm: no pair" => no_tac)
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   973
    | _ => no_tac)
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   974
*}
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   975
ML {*
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   976
fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   977
*}
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   978
33ff4b5f1806 puting code in separate sections
Christian Urban <urbanc@in.tum.de>
parents: 575
diff changeset
   979
ML {*
548
9fb773ec083c Changed FOCUS to SUBGOAL in rep_abs_rsp_tac; another 20% speedup :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 547
diff changeset
   980
fun rep_abs_rsp_tac ctxt =
9fb773ec083c Changed FOCUS to SUBGOAL in rep_abs_rsp_tac; another 20% speedup :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 547
diff changeset
   981
  SUBGOAL (fn (goal, i) =>
551
34d12737b379 tuned code
Christian Urban <urbanc@in.tum.de>
parents: 550
diff changeset
   982
    case (bare_concl goal) of 
34d12737b379 tuned code
Christian Urban <urbanc@in.tum.de>
parents: 550
diff changeset
   983
      (rel $ _ $ (rep $ (abs $ _))) =>
34d12737b379 tuned code
Christian Urban <urbanc@in.tum.de>
parents: 550
diff changeset
   984
        (let
34d12737b379 tuned code
Christian Urban <urbanc@in.tum.de>
parents: 550
diff changeset
   985
           val thy = ProofContext.theory_of ctxt;
34d12737b379 tuned code
Christian Urban <urbanc@in.tum.de>
parents: 550
diff changeset
   986
           val (ty_a, ty_b) = dest_fun_type (fastype_of abs);
34d12737b379 tuned code
Christian Urban <urbanc@in.tum.de>
parents: 550
diff changeset
   987
           val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
34d12737b379 tuned code
Christian Urban <urbanc@in.tum.de>
parents: 550
diff changeset
   988
           val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep];
34d12737b379 tuned code
Christian Urban <urbanc@in.tum.de>
parents: 550
diff changeset
   989
           val thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp}
34d12737b379 tuned code
Christian Urban <urbanc@in.tum.de>
parents: 550
diff changeset
   990
           val te = solve_quotient_assums ctxt thm
34d12737b379 tuned code
Christian Urban <urbanc@in.tum.de>
parents: 550
diff changeset
   991
         in
34d12737b379 tuned code
Christian Urban <urbanc@in.tum.de>
parents: 550
diff changeset
   992
           rtac te i
34d12737b379 tuned code
Christian Urban <urbanc@in.tum.de>
parents: 550
diff changeset
   993
         end
34d12737b379 tuned code
Christian Urban <urbanc@in.tum.de>
parents: 550
diff changeset
   994
         handle _ => no_tac)
34d12737b379 tuned code
Christian Urban <urbanc@in.tum.de>
parents: 550
diff changeset
   995
    | _ => no_tac)
522
6b77cfd508e9 rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 519
diff changeset
   996
*}
6b77cfd508e9 rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 519
diff changeset
   997
512
8c7597b19f0e First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 505
diff changeset
   998
ML {*
525
3f657c4fbefa Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 523
diff changeset
   999
fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) =>
551
34d12737b379 tuned code
Christian Urban <urbanc@in.tum.de>
parents: 550
diff changeset
  1000
(case (bare_concl goal) of
525
3f657c4fbefa Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 523
diff changeset
  1001
    (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
536
44fa9df44e6f More code cleaning and name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 529
diff changeset
  1002
  ((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _))
44fa9df44e6f More code cleaning and name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 529
diff changeset
  1003
      => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
577
8dab8d82f26b more tuning of the code
Christian Urban <urbanc@in.tum.de>
parents: 576
diff changeset
  1004
525
3f657c4fbefa Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 523
diff changeset
  1005
    (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
512
8c7597b19f0e First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 505
diff changeset
  1006
| (Const (@{const_name "op ="},_) $
8c7597b19f0e First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 505
diff changeset
  1007
    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
8c7597b19f0e First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 505
diff changeset
  1008
    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
8c7597b19f0e First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 505
diff changeset
  1009
      => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
577
8dab8d82f26b more tuning of the code
Christian Urban <urbanc@in.tum.de>
parents: 576
diff changeset
  1010
525
3f657c4fbefa Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 523
diff changeset
  1011
    (* (R1 ===> op =) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Ball\<dots>x) = (Ball\<dots>y) *)
536
44fa9df44e6f More code cleaning and name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 529
diff changeset
  1012
| (Const (@{const_name fun_rel}, _) $ _ $ _) $
512
8c7597b19f0e First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 505
diff changeset
  1013
    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
8c7597b19f0e First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 505
diff changeset
  1014
    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
536
44fa9df44e6f More code cleaning and name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 529
diff changeset
  1015
      => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
577
8dab8d82f26b more tuning of the code
Christian Urban <urbanc@in.tum.de>
parents: 576
diff changeset
  1016
525
3f657c4fbefa Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 523
diff changeset
  1017
    (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
512
8c7597b19f0e First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 505
diff changeset
  1018
| Const (@{const_name "op ="},_) $
8c7597b19f0e First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 505
diff changeset
  1019
    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
8c7597b19f0e First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 505
diff changeset
  1020
    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
8c7597b19f0e First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 505
diff changeset
  1021
      => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
577
8dab8d82f26b more tuning of the code
Christian Urban <urbanc@in.tum.de>
parents: 576
diff changeset
  1022
525
3f657c4fbefa Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 523
diff changeset
  1023
    (* (R1 ===> op =) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Bex\<dots>x) = (Bex\<dots>y) *)
536
44fa9df44e6f More code cleaning and name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 529
diff changeset
  1024
| (Const (@{const_name fun_rel}, _) $ _ $ _) $
512
8c7597b19f0e First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 505
diff changeset
  1025
    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
8c7597b19f0e First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 505
diff changeset
  1026
    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
536
44fa9df44e6f More code cleaning and name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 529
diff changeset
  1027
      => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
577
8dab8d82f26b more tuning of the code
Christian Urban <urbanc@in.tum.de>
parents: 576
diff changeset
  1028
525
3f657c4fbefa Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 523
diff changeset
  1029
    (* reflexivity of operators arising from Cong_tac *)
577
8dab8d82f26b more tuning of the code
Christian Urban <urbanc@in.tum.de>
parents: 576
diff changeset
  1030
| Const (@{const_name "op ="},_) $ _ $ _ 
8dab8d82f26b more tuning of the code
Christian Urban <urbanc@in.tum.de>
parents: 576
diff changeset
  1031
      => rtac @{thm refl} ORELSE'
8dab8d82f26b more tuning of the code
Christian Urban <urbanc@in.tum.de>
parents: 576
diff changeset
  1032
          (resolve_tac trans2 THEN' RANGE [
8dab8d82f26b more tuning of the code
Christian Urban <urbanc@in.tum.de>
parents: 576
diff changeset
  1033
            quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])
8dab8d82f26b more tuning of the code
Christian Urban <urbanc@in.tum.de>
parents: 576
diff changeset
  1034
561
41500cd131dc Added nil_rsp and cons_rsp to quotient_rsp; simplified IntEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 559
diff changeset
  1035
| (Const (@{const_name fun_rel}, _) $ _ $ _) $
41500cd131dc Added nil_rsp and cons_rsp to quotient_rsp; simplified IntEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 559
diff changeset
  1036
    (Const (@{const_name fun_rel}, _) $ _ $ _) $
41500cd131dc Added nil_rsp and cons_rsp to quotient_rsp; simplified IntEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 559
diff changeset
  1037
    (Const (@{const_name fun_rel}, _) $ _ $ _)
41500cd131dc Added nil_rsp and cons_rsp to quotient_rsp; simplified IntEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 559
diff changeset
  1038
    => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt
577
8dab8d82f26b more tuning of the code
Christian Urban <urbanc@in.tum.de>
parents: 576
diff changeset
  1039
8dab8d82f26b more tuning of the code
Christian Urban <urbanc@in.tum.de>
parents: 576
diff changeset
  1040
   (* respectfulness of constants; in particular of a simple relation *)
8dab8d82f26b more tuning of the code
Christian Urban <urbanc@in.tum.de>
parents: 576
diff changeset
  1041
| _ $ (Const _) $ (Const _)  (* fun_rel, list_rel, etc but not equality *)
8dab8d82f26b more tuning of the code
Christian Urban <urbanc@in.tum.de>
parents: 576
diff changeset
  1042
    => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
8dab8d82f26b more tuning of the code
Christian Urban <urbanc@in.tum.de>
parents: 576
diff changeset
  1043
525
3f657c4fbefa Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 523
diff changeset
  1044
    (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
3f657c4fbefa Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 523
diff changeset
  1045
    (* observe ---> *)
577
8dab8d82f26b more tuning of the code
Christian Urban <urbanc@in.tum.de>
parents: 576
diff changeset
  1046
| _ $ _ $ _ 
8dab8d82f26b more tuning of the code
Christian Urban <urbanc@in.tum.de>
parents: 576
diff changeset
  1047
    => rep_abs_rsp_tac ctxt
8dab8d82f26b more tuning of the code
Christian Urban <urbanc@in.tum.de>
parents: 576
diff changeset
  1048
522
6b77cfd508e9 rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 519
diff changeset
  1049
| _ => error "inj_repabs_tac not a relation"
512
8c7597b19f0e First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 505
diff changeset
  1050
) i)
8c7597b19f0e First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 505
diff changeset
  1051
*}
8c7597b19f0e First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 505
diff changeset
  1052
8c7597b19f0e First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 505
diff changeset
  1053
ML {*
525
3f657c4fbefa Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 523
diff changeset
  1054
fun inj_repabs_tac ctxt rel_refl trans2 =
512
8c7597b19f0e First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 505
diff changeset
  1055
  (FIRST' [
525
3f657c4fbefa Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 523
diff changeset
  1056
    inj_repabs_tac_match ctxt trans2,
527
9b1ad366827f code cleaning and renaming
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 526
diff changeset
  1057
    (* R (t $ \<dots>) (t' $ \<dots>) ----> apply_rsp   provided type of t needs lifting *)
9b1ad366827f code cleaning and renaming
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 526
diff changeset
  1058
    NDT ctxt "A" (apply_rsp_tac ctxt THEN'
517
ede7f9622a54 Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 516
diff changeset
  1059
                (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
525
3f657c4fbefa Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 523
diff changeset
  1060
    (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong   provided type of t does not need lifting *)
3f657c4fbefa Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 523
diff changeset
  1061
    (* merge with previous tactic *)
512
8c7597b19f0e First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 505
diff changeset
  1062
    NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN'
8c7597b19f0e First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 505
diff changeset
  1063
                (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
525
3f657c4fbefa Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 523
diff changeset
  1064
    (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
512
8c7597b19f0e First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 505
diff changeset
  1065
    NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam),
525
3f657c4fbefa Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 523
diff changeset
  1066
    (* resolving with R x y assumptions *)
512
8c7597b19f0e First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 505
diff changeset
  1067
    NDT ctxt "E" (atac),
525
3f657c4fbefa Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 523
diff changeset
  1068
    (* reflexivity of the basic relations *)
3f657c4fbefa Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 523
diff changeset
  1069
    (* R \<dots> \<dots> *)
555
b460565dbb58 Handling of respects in the fast inj_repabs_tac; includes respects with quotient assumptions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 554
diff changeset
  1070
    NDT ctxt "D" (resolve_tac rel_refl)
515
b00a9b58264d Fixes after big merge.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 514
diff changeset
  1071
    ])
512
8c7597b19f0e First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 505
diff changeset
  1072
*}
8c7597b19f0e First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 505
diff changeset
  1073
8c7597b19f0e First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 505
diff changeset
  1074
ML {*
525
3f657c4fbefa Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 523
diff changeset
  1075
fun all_inj_repabs_tac ctxt rel_refl trans2 =
3f657c4fbefa Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 523
diff changeset
  1076
  REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2)
512
8c7597b19f0e First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 505
diff changeset
  1077
*}
8c7597b19f0e First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 505
diff changeset
  1078
399
646bfe5905b3 tuned comments
Christian Urban <urbanc@in.tum.de>
parents: 398
diff changeset
  1079
section {* Cleaning of the theorem *}
387
f78aa16daae5 reordered the code
Christian Urban <urbanc@in.tum.de>
parents: 386
diff changeset
  1080
f78aa16daae5 reordered the code
Christian Urban <urbanc@in.tum.de>
parents: 386
diff changeset
  1081
ML {*
440
0af649448a11 Moved fast instantiation to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 436
diff changeset
  1082
fun make_inst lhs t =
0af649448a11 Moved fast instantiation to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 436
diff changeset
  1083
  let
0af649448a11 Moved fast instantiation to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 436
diff changeset
  1084
    val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
0af649448a11 Moved fast instantiation to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 436
diff changeset
  1085
    val _ $ (Abs (_, _, g)) = t;
0af649448a11 Moved fast instantiation to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 436
diff changeset
  1086
    fun mk_abs i t =
0af649448a11 Moved fast instantiation to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 436
diff changeset
  1087
      if incr_boundvars i u aconv t then Bound i
0af649448a11 Moved fast instantiation to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 436
diff changeset
  1088
      else (case t of
0af649448a11 Moved fast instantiation to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 436
diff changeset
  1089
        t1 $ t2 => mk_abs i t1 $ mk_abs i t2
469
6d077eac6ad7 QUOT_TRUE joke
Christian Urban <urbanc@in.tum.de>
parents: 468
diff changeset
  1090
      | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t')
440
0af649448a11 Moved fast instantiation to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 436
diff changeset
  1091
      | Bound j => if i = j then error "make_inst" else t
0af649448a11 Moved fast instantiation to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 436
diff changeset
  1092
      | _ => t);
0af649448a11 Moved fast instantiation to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 436
diff changeset
  1093
  in (f, Abs ("x", T, mk_abs 0 g)) end;
490
5214ec75add4 simplified lambda_prs_conv
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1094
*}
440
0af649448a11 Moved fast instantiation to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 436
diff changeset
  1095
492
6793659d38d6 Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 491
diff changeset
  1096
ML {*
571
9c6991411e1f renamed lambda_allex_prs
Christian Urban <urbanc@in.tum.de>
parents: 569
diff changeset
  1097
fun lambda_prs_simple_conv ctxt ctrm =
492
6793659d38d6 Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 491
diff changeset
  1098
  case (term_of ctrm) of
586
cdc6ae1a4ed2 fixed examples
Christian Urban <urbanc@in.tum.de>
parents: 583
diff changeset
  1099
   ((Const (@{const_name fun_map}, _) $ r1 $ (a2 as (Const (s,_)))) $ (Abs _)) =>
572
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1100
     let
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1101
       val thy = ProofContext.theory_of ctxt
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1102
       val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1103
       val (ty_c, ty_d) = dest_fun_type (fastype_of a2)
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1104
       val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1105
       val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1106
       val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs}
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1107
       val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)]
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1108
       val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1109
       val tl = Thm.lhs_of ts
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1110
       val (insp, inst) = make_inst (term_of tl) (term_of ctrm)
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1111
       val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
586
cdc6ae1a4ed2 fixed examples
Christian Urban <urbanc@in.tum.de>
parents: 583
diff changeset
  1112
       val _ = if not (s = @{const_name "id"}) then
cdc6ae1a4ed2 fixed examples
Christian Urban <urbanc@in.tum.de>
parents: 583
diff changeset
  1113
                  (tracing "lambda_prs";
cdc6ae1a4ed2 fixed examples
Christian Urban <urbanc@in.tum.de>
parents: 583
diff changeset
  1114
                   tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)));
cdc6ae1a4ed2 fixed examples
Christian Urban <urbanc@in.tum.de>
parents: 583
diff changeset
  1115
                   tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi)));
cdc6ae1a4ed2 fixed examples
Christian Urban <urbanc@in.tum.de>
parents: 583
diff changeset
  1116
                   tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te)));
cdc6ae1a4ed2 fixed examples
Christian Urban <urbanc@in.tum.de>
parents: 583
diff changeset
  1117
                   tracing ("ts rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ts)));
cdc6ae1a4ed2 fixed examples
Christian Urban <urbanc@in.tum.de>
parents: 583
diff changeset
  1118
                   tracing ("instantiated rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti))))
cdc6ae1a4ed2 fixed examples
Christian Urban <urbanc@in.tum.de>
parents: 583
diff changeset
  1119
               else ()
572
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1120
     in
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1121
       Conv.rewr_conv ti ctrm
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1122
     end
490
5214ec75add4 simplified lambda_prs_conv
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1123
  | _ => Conv.all_conv ctrm
387
f78aa16daae5 reordered the code
Christian Urban <urbanc@in.tum.de>
parents: 386
diff changeset
  1124
*}
f78aa16daae5 reordered the code
Christian Urban <urbanc@in.tum.de>
parents: 386
diff changeset
  1125
f78aa16daae5 reordered the code
Christian Urban <urbanc@in.tum.de>
parents: 386
diff changeset
  1126
ML {*
571
9c6991411e1f renamed lambda_allex_prs
Christian Urban <urbanc@in.tum.de>
parents: 569
diff changeset
  1127
val lambda_prs_conv =
9c6991411e1f renamed lambda_allex_prs
Christian Urban <urbanc@in.tum.de>
parents: 569
diff changeset
  1128
  More_Conv.top_conv lambda_prs_simple_conv
387
f78aa16daae5 reordered the code
Christian Urban <urbanc@in.tum.de>
parents: 386
diff changeset
  1129
571
9c6991411e1f renamed lambda_allex_prs
Christian Urban <urbanc@in.tum.de>
parents: 569
diff changeset
  1130
fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
387
f78aa16daae5 reordered the code
Christian Urban <urbanc@in.tum.de>
parents: 386
diff changeset
  1131
*}
f78aa16daae5 reordered the code
Christian Urban <urbanc@in.tum.de>
parents: 386
diff changeset
  1132
457
48042bacdce2 Commented clean-tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 455
diff changeset
  1133
(*
572
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1134
 Cleaning the theorem consists of three rewriting steps.
465
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 464
diff changeset
  1135
 The first two need to be done before fun_map is unfolded
457
48042bacdce2 Commented clean-tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 455
diff changeset
  1136
572
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1137
 1) lambda_prs:
469
6d077eac6ad7 QUOT_TRUE joke
Christian Urban <urbanc@in.tum.de>
parents: 468
diff changeset
  1138
     (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))  ---->  f
6d077eac6ad7 QUOT_TRUE joke
Christian Urban <urbanc@in.tum.de>
parents: 468
diff changeset
  1139
572
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1140
    Implemented as conversion since it is not a pattern.
469
6d077eac6ad7 QUOT_TRUE joke
Christian Urban <urbanc@in.tum.de>
parents: 468
diff changeset
  1141
572
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1142
 2) all_prs (the same for exists):
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1143
     Ball (Respects R) ((abs ---> id) f)  ---->  All f
469
6d077eac6ad7 QUOT_TRUE joke
Christian Urban <urbanc@in.tum.de>
parents: 468
diff changeset
  1144
572
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1145
    Rewriting with definitions from the argument defs
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1146
     (rep ---> abs) oldConst ----> newconst
469
6d077eac6ad7 QUOT_TRUE joke
Christian Urban <urbanc@in.tum.de>
parents: 468
diff changeset
  1147
572
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1148
 3) Quotient_rel_rep:
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1149
      Rel (Rep x) (Rep y)  ---->  x = y
469
6d077eac6ad7 QUOT_TRUE joke
Christian Urban <urbanc@in.tum.de>
parents: 468
diff changeset
  1150
572
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1151
    Quotient_abs_rep:
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1152
      Abs (Rep x)  ---->  x
457
48042bacdce2 Commented clean-tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 455
diff changeset
  1153
572
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1154
    id_simps; fun_map.simps
457
48042bacdce2 Commented clean-tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 455
diff changeset
  1155
*)
469
6d077eac6ad7 QUOT_TRUE joke
Christian Urban <urbanc@in.tum.de>
parents: 468
diff changeset
  1156
556
287ea842a7d4 simpler version of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 552
diff changeset
  1157
ML {*
506
91c374abde06 removed quot argument...not all examples work anymore
Christian Urban <urbanc@in.tum.de>
parents: 505
diff changeset
  1158
fun clean_tac lthy =
387
f78aa16daae5 reordered the code
Christian Urban <urbanc@in.tum.de>
parents: 386
diff changeset
  1159
  let
498
e7bb6bbe7576 defs used automatically by clean_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 495
diff changeset
  1160
    val thy = ProofContext.theory_of lthy;
566
4eca2c3e59f7 Used symmetric definitions. Moved quotient_rsp to QuotMain.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 564
diff changeset
  1161
    val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
572
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1162
      (* FIXME: shouldn't the definitions already be varified? *)
567
5dffcd087e30 Definitions folded first.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 566
diff changeset
  1163
    val thms1 = @{thms all_prs ex_prs} @ defs
564
96c241932603 moved all_prs and ex_prs out from the conversion into the simplifier
Christian Urban <urbanc@in.tum.de>
parents: 563
diff changeset
  1164
    val thms2 = @{thms eq_reflection[OF fun_map.simps]} 
96c241932603 moved all_prs and ex_prs out from the conversion into the simplifier
Christian Urban <urbanc@in.tum.de>
parents: 563
diff changeset
  1165
                @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} 
588
2c95d0436a2b removed usage of HOL_basic_ss by using a slighly extended version of empty_ss
Christian Urban <urbanc@in.tum.de>
parents: 586
diff changeset
  1166
    fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
387
f78aa16daae5 reordered the code
Christian Urban <urbanc@in.tum.de>
parents: 386
diff changeset
  1167
  in
572
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1168
    EVERY' [lambda_prs_tac lthy,
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1169
            simp_tac (simps thms1),
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1170
            simp_tac (simps thms2),
a68c51dd85b3 working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
parents: 571
diff changeset
  1171
            TRY o rtac refl]
387
f78aa16daae5 reordered the code
Christian Urban <urbanc@in.tum.de>
parents: 386
diff changeset
  1172
  end
f78aa16daae5 reordered the code
Christian Urban <urbanc@in.tum.de>
parents: 386
diff changeset
  1173
*}
381
991db758a72d More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 379
diff changeset
  1174
404
d676974e3c89 more tuning
Christian Urban <urbanc@in.tum.de>
parents: 403
diff changeset
  1175
section {* Genralisation of free variables in a goal *}
347
7e82493c6253 Finished temporary goal-directed lift_theorem wrapper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 346
diff changeset
  1176
7e82493c6253 Finished temporary goal-directed lift_theorem wrapper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 346
diff changeset
  1177
ML {*
374
980fdf92a834 fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents: 372
diff changeset
  1178
fun inst_spec ctrm =
411
c10e314761fa simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
parents: 410
diff changeset
  1179
   Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
374
980fdf92a834 fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents: 372
diff changeset
  1180
980fdf92a834 fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents: 372
diff changeset
  1181
fun inst_spec_tac ctrms =
980fdf92a834 fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents: 372
diff changeset
  1182
  EVERY' (map (dtac o inst_spec) ctrms)
980fdf92a834 fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents: 372
diff changeset
  1183
412
54d3c72ddd05 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 411
diff changeset
  1184
fun all_list xs trm = 
411
c10e314761fa simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
parents: 410
diff changeset
  1185
  fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm
c10e314761fa simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
parents: 410
diff changeset
  1186
c10e314761fa simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
parents: 410
diff changeset
  1187
fun apply_under_Trueprop f = 
c10e314761fa simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
parents: 410
diff changeset
  1188
  HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop
362
7a3d86050e72 added a prepare_tac
Christian Urban <urbanc@in.tum.de>
parents: 360
diff changeset
  1189
374
980fdf92a834 fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents: 372
diff changeset
  1190
fun gen_frees_tac ctxt =
980fdf92a834 fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents: 372
diff changeset
  1191
 SUBGOAL (fn (concl, i) =>
980fdf92a834 fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents: 372
diff changeset
  1192
  let
980fdf92a834 fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents: 372
diff changeset
  1193
    val thy = ProofContext.theory_of ctxt
411
c10e314761fa simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
parents: 410
diff changeset
  1194
    val vrs = Term.add_frees concl []
374
980fdf92a834 fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents: 372
diff changeset
  1195
    val cvrs = map (cterm_of thy o Free) vrs
412
54d3c72ddd05 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 411
diff changeset
  1196
    val concl' = apply_under_Trueprop (all_list vrs) concl
411
c10e314761fa simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
parents: 410
diff changeset
  1197
    val goal = Logic.mk_implies (concl', concl)
374
980fdf92a834 fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents: 372
diff changeset
  1198
    val rule = Goal.prove ctxt [] [] goal 
411
c10e314761fa simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
parents: 410
diff changeset
  1199
      (K (EVERY1 [inst_spec_tac (rev cvrs), atac]))
374
980fdf92a834 fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents: 372
diff changeset
  1200
  in
980fdf92a834 fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents: 372
diff changeset
  1201
    rtac rule i
980fdf92a834 fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents: 372
diff changeset
  1202
  end)  
362
7a3d86050e72 added a prepare_tac
Christian Urban <urbanc@in.tum.de>
parents: 360
diff changeset
  1203
*}
7a3d86050e72 added a prepare_tac
Christian Urban <urbanc@in.tum.de>
parents: 360
diff changeset
  1204
402
dd64cca9265c recommited changes of comments
Christian Urban <urbanc@in.tum.de>
parents: 401
diff changeset
  1205
section {* General outline of the lifting procedure *}
dd64cca9265c recommited changes of comments
Christian Urban <urbanc@in.tum.de>
parents: 401
diff changeset
  1206
383
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
  1207
(* - A is the original raw theorem          *)
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
  1208
(* - B is the regularized theorem           *)
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
  1209
(* - C is the rep/abs injected version of B *) 
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
  1210
(* - D is the lifted theorem                *)
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
  1211
(*                                          *)
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
  1212
(* - b is the regularization step           *)
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
  1213
(* - c is the rep/abs injection step        *)
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
  1214
(* - d is the cleaning part                 *)
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
  1215
413
Christian Urban <urbanc@in.tum.de>
parents: 412
diff changeset
  1216
lemma lifting_procedure:
360
07fb696efa3d Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 359
diff changeset
  1217
  assumes a: "A"
07fb696efa3d Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 359
diff changeset
  1218
  and     b: "A \<Longrightarrow> B"
07fb696efa3d Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 359
diff changeset
  1219
  and     c: "B = C"
07fb696efa3d Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 359
diff changeset
  1220
  and     d: "C = D"
07fb696efa3d Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 359
diff changeset
  1221
  shows   "D"
07fb696efa3d Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 359
diff changeset
  1222
  using a b c d
07fb696efa3d Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 359
diff changeset
  1223
  by simp
07fb696efa3d Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 359
diff changeset
  1224
374
980fdf92a834 fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents: 372
diff changeset
  1225
ML {*
412
54d3c72ddd05 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 411
diff changeset
  1226
fun lift_match_error ctxt fun_str rtrm qtrm =
374
980fdf92a834 fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents: 372
diff changeset
  1227
let
980fdf92a834 fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents: 372
diff changeset
  1228
  val rtrm_str = Syntax.string_of_term ctxt rtrm
980fdf92a834 fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents: 372
diff changeset
  1229
  val qtrm_str = Syntax.string_of_term ctxt qtrm
388
aa452130ae7f polishing
Christian Urban <urbanc@in.tum.de>
parents: 387
diff changeset
  1230
  val msg = [enclose "[" "]" fun_str, "The quotient theorem\n", qtrm_str, 
aa452130ae7f polishing
Christian Urban <urbanc@in.tum.de>
parents: 387
diff changeset
  1231
             "and the lifted theorem\n", rtrm_str, "do not match"]
374
980fdf92a834 fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents: 372
diff changeset
  1232
in
980fdf92a834 fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents: 372
diff changeset
  1233
  error (space_implode " " msg)
980fdf92a834 fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents: 372
diff changeset
  1234
end
980fdf92a834 fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents: 372
diff changeset
  1235
*}
980fdf92a834 fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents: 372
diff changeset
  1236
360
07fb696efa3d Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 359
diff changeset
  1237
ML {* 
07fb696efa3d Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 359
diff changeset
  1238
fun procedure_inst ctxt rtrm qtrm =
07fb696efa3d Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 359
diff changeset
  1239
let
07fb696efa3d Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 359
diff changeset
  1240
  val thy = ProofContext.theory_of ctxt
07fb696efa3d Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 359
diff changeset
  1241
  val rtrm' = HOLogic.dest_Trueprop rtrm
07fb696efa3d Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 359
diff changeset
  1242
  val qtrm' = HOLogic.dest_Trueprop qtrm
383
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
  1243
  val reg_goal = 
405
8bc7428745ad renamed REGULARIZE to be regularize
Christian Urban <urbanc@in.tum.de>
parents: 404
diff changeset
  1244
        Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm')
412
54d3c72ddd05 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 411
diff changeset
  1245
        handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm
564
96c241932603 moved all_prs and ex_prs out from the conversion into the simplifier
Christian Urban <urbanc@in.tum.de>
parents: 563
diff changeset
  1246
  val _ = warning "Regularization done."
383
73a3670fb00e comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents: 382
diff changeset
  1247
  val inj_goal = 
408
1056861b562c renamed inj_REPABS to inj_repabs_trm
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
  1248
        Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm'))
412
54d3c72ddd05 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 411
diff changeset
  1249
        handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm
564
96c241932603 moved all_prs and ex_prs out from the conversion into the simplifier
Christian Urban <urbanc@in.tum.de>
parents: 563
diff changeset
  1250
  val _ = warning "RepAbs Injection done."
360
07fb696efa3d Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 359
diff changeset
  1251
in
07fb696efa3d Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 359
diff changeset
  1252
  Drule.instantiate' []
07fb696efa3d Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 359
diff changeset
  1253
    [SOME (cterm_of thy rtrm'),
07fb696efa3d Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 359
diff changeset
  1254
     SOME (cterm_of thy reg_goal),
413
Christian Urban <urbanc@in.tum.de>
parents: 412
diff changeset
  1255
     SOME (cterm_of thy inj_goal)] @{thm lifting_procedure}
360
07fb696efa3d Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 359
diff changeset
  1256
end
362
7a3d86050e72 added a prepare_tac
Christian Urban <urbanc@in.tum.de>
parents: 360
diff changeset
  1257
*}
389
d67240113f68 applic_prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 388
diff changeset
  1258
d67240113f68 applic_prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 388
diff changeset
  1259
(* Left for debugging *)
362
7a3d86050e72 added a prepare_tac
Christian Urban <urbanc@in.tum.de>
parents: 360
diff changeset
  1260
ML {*
547
b0809b256a88 Changing FOCUS to CSUBGOAL (part 1)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 544
diff changeset
  1261
fun procedure_tac ctxt rthm =
389
d67240113f68 applic_prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 388
diff changeset
  1262
  ObjectLogic.full_atomize_tac
547
b0809b256a88 Changing FOCUS to CSUBGOAL (part 1)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 544
diff changeset
  1263
  THEN' gen_frees_tac ctxt
b0809b256a88 Changing FOCUS to CSUBGOAL (part 1)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 544
diff changeset
  1264
  THEN' CSUBGOAL (fn (gl, i) =>
389
d67240113f68 applic_prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 388
diff changeset
  1265
    let
d67240113f68 applic_prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 388
diff changeset
  1266
      val rthm' = atomize_thm rthm
547
b0809b256a88 Changing FOCUS to CSUBGOAL (part 1)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 544
diff changeset
  1267
      val rule = procedure_inst ctxt (prop_of rthm') (term_of gl)
b0809b256a88 Changing FOCUS to CSUBGOAL (part 1)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 544
diff changeset
  1268
      val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i}
389
d67240113f68 applic_prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 388
diff changeset
  1269
    in
547
b0809b256a88 Changing FOCUS to CSUBGOAL (part 1)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 544
diff changeset
  1270
      (rtac rule THEN' RANGE [rtac rthm', (fn _ => all_tac), rtac thm]) i
b0809b256a88 Changing FOCUS to CSUBGOAL (part 1)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 544
diff changeset
  1271
    end)
360
07fb696efa3d Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 359
diff changeset
  1272
*}
07fb696efa3d Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 359
diff changeset
  1273
361
e9bcbdeb3a1e TRY' for clean_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 360
diff changeset
  1274
ML {*
413
Christian Urban <urbanc@in.tum.de>
parents: 412
diff changeset
  1275
(* FIXME/TODO should only get as arguments the rthm like procedure_tac *)
489
2b7b349e470f deleted now obsolete argument rty everywhere
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
  1276
582
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
  1277
fun lift_tac ctxt rthm =
389
d67240113f68 applic_prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 388
diff changeset
  1278
  ObjectLogic.full_atomize_tac
547
b0809b256a88 Changing FOCUS to CSUBGOAL (part 1)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 544
diff changeset
  1279
  THEN' gen_frees_tac ctxt
b0809b256a88 Changing FOCUS to CSUBGOAL (part 1)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 544
diff changeset
  1280
  THEN' CSUBGOAL (fn (gl, i) =>
389
d67240113f68 applic_prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 388
diff changeset
  1281
    let
d67240113f68 applic_prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 388
diff changeset
  1282
      val rthm' = atomize_thm rthm
547
b0809b256a88 Changing FOCUS to CSUBGOAL (part 1)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 544
diff changeset
  1283
      val rule = procedure_inst ctxt (prop_of rthm') (term_of gl)
582
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
  1284
      val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) (equiv_rules_get ctxt)
547
b0809b256a88 Changing FOCUS to CSUBGOAL (part 1)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 544
diff changeset
  1285
      val quotients = quotient_rules_get ctxt
527
9b1ad366827f code cleaning and renaming
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 526
diff changeset
  1286
      val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quotients
547
b0809b256a88 Changing FOCUS to CSUBGOAL (part 1)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 544
diff changeset
  1287
      val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i}
389
d67240113f68 applic_prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 388
diff changeset
  1288
    in
547
b0809b256a88 Changing FOCUS to CSUBGOAL (part 1)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 544
diff changeset
  1289
      (rtac rule THEN'
b0809b256a88 Changing FOCUS to CSUBGOAL (part 1)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 544
diff changeset
  1290
       RANGE [rtac rthm',
582
a082e2d138ab added a theorem list for equivalence theorems
Christian Urban <urbanc@in.tum.de>
parents: 578
diff changeset
  1291
              regularize_tac ctxt,
547
b0809b256a88 Changing FOCUS to CSUBGOAL (part 1)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 544
diff changeset
  1292
              rtac thm THEN' all_inj_repabs_tac ctxt rel_refl trans2,
b0809b256a88 Changing FOCUS to CSUBGOAL (part 1)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 544
diff changeset
  1293
              clean_tac ctxt]) i
b0809b256a88 Changing FOCUS to CSUBGOAL (part 1)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 544
diff changeset
  1294
    end)
361
e9bcbdeb3a1e TRY' for clean_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 360
diff changeset
  1295
*}
e9bcbdeb3a1e TRY' for clean_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 360
diff changeset
  1296
198
ff4425e000db Completely cleaned Int.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 197
diff changeset
  1297
end
239
02b14a21761a Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 236
diff changeset
  1298