QuotMain.thy
author Christian Urban <urbanc@in.tum.de>
Mon, 12 Oct 2009 23:39:14 +0200
changeset 81 c8d58e2cda58
parent 80 3a68c1693a32
child 84 21825adc3c22
permissions -rw-r--r--
slightly modified the parser
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
71
35be65791f1d exported parts of QuotMain into a separate ML-file
Christian Urban <urbanc@in.tum.de>
parents: 70
diff changeset
     3
uses ("quotient.ML")
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
begin
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
locale QUOT_TYPE =
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     7
  fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     8
  and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     9
  and   Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    10
  assumes equiv: "EQUIV R"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    11
  and     rep_prop: "\<And>y. \<exists>x. Rep y = R x"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    12
  and     rep_inverse: "\<And>x. Abs (Rep x) = x"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    13
  and     abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    14
  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
    15
begin
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    16
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    17
definition
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    18
  "ABS x \<equiv> Abs (R x)"
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
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    21
  "REP a = Eps (Rep a)"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    22
15
f46eddb570a3 Cleaning the code
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 14
diff changeset
    23
lemma lem9:
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    24
  shows "R (Eps (R x)) = R x"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    25
proof -
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    26
  have a: "R x x" using equiv by (simp add: EQUIV_REFL_SYM_TRANS REFL_def)
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    27
  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
    28
  then show "R (Eps (R x)) = R x"
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    29
    using equiv unfolding EQUIV_def by simp
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    30
qed
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    31
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    32
theorem thm10:
24
6885fa184e89 Merged with my changes from the morning:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 23
diff changeset
    33
  shows "ABS (REP a) \<equiv> a"
6885fa184e89 Merged with my changes from the morning:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 23
diff changeset
    34
  apply  (rule eq_reflection)
6885fa184e89 Merged with my changes from the morning:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 23
diff changeset
    35
  unfolding ABS_def REP_def
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    36
proof -
15
f46eddb570a3 Cleaning the code
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 14
diff changeset
    37
  from rep_prop
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    38
  obtain x where eq: "Rep a = R x" by auto
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    39
  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
    40
  also have "\<dots> = Abs (R x)" using lem9 by simp
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    41
  also have "\<dots> = Abs (Rep a)" using eq by simp
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    42
  also have "\<dots> = a" using rep_inverse by simp
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    43
  finally
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    44
  show "Abs (R (Eps (Rep a))) = a" by simp
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    45
qed
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    46
15
f46eddb570a3 Cleaning the code
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 14
diff changeset
    47
lemma REP_refl:
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    48
  shows "R (REP a) (REP a)"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    49
unfolding REP_def
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    50
by (simp add: equiv[simplified EQUIV_def])
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    51
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    52
lemma lem7:
22
5023bf36d81a beautification of some proofs
Ning@localhost
parents: 21
diff changeset
    53
  shows "(R x = R y) = (Abs (R x) = Abs (R y))"
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    54
apply(rule iffI)
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    55
apply(simp)
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    56
apply(drule rep_inject[THEN iffD2])
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    57
apply(simp add: abs_inverse)
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    58
done
15
f46eddb570a3 Cleaning the code
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 14
diff changeset
    59
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    60
theorem thm11:
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    61
  shows "R r r' = (ABS r = ABS r')"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    62
unfolding ABS_def
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    63
by (simp only: equiv[simplified EQUIV_def] lem7)
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    64
4
Christian Urban <urbanc@in.tum.de>
parents: 3
diff changeset
    65
2
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
    66
lemma REP_ABS_rsp:
4
Christian Urban <urbanc@in.tum.de>
parents: 3
diff changeset
    67
  shows "R f (REP (ABS g)) = R f g"
Christian Urban <urbanc@in.tum.de>
parents: 3
diff changeset
    68
  and   "R (REP (ABS g)) f = R g f"
23
f6c6cf8c3b98 some more beautification
Ning@localhost
parents: 22
diff changeset
    69
by (simp_all add: thm10 thm11)
4
Christian Urban <urbanc@in.tum.de>
parents: 3
diff changeset
    70
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    71
lemma QUOTIENT:
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    72
  "QUOTIENT R ABS REP"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    73
apply(unfold QUOTIENT_def)
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    74
apply(simp add: thm10)
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    75
apply(simp add: REP_refl)
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    76
apply(subst thm11[symmetric])
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    77
apply(simp add: equiv[simplified EQUIV_def])
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    78
done
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    79
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
    80
lemma R_trans:
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
    81
  assumes ab: "R a b"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
    82
  and     bc: "R b c"
22
5023bf36d81a beautification of some proofs
Ning@localhost
parents: 21
diff changeset
    83
  shows "R a c"
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
    84
proof -
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
    85
  have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
    86
  moreover have ab: "R a b" by fact
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
    87
  moreover have bc: "R b c" by fact
22
5023bf36d81a beautification of some proofs
Ning@localhost
parents: 21
diff changeset
    88
  ultimately show "R a c" unfolding TRANS_def by blast
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
    89
qed
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
    90
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
    91
lemma R_sym:
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
    92
  assumes ab: "R a b"
22
5023bf36d81a beautification of some proofs
Ning@localhost
parents: 21
diff changeset
    93
  shows "R b a"
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
    94
proof -
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
    95
  have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
22
5023bf36d81a beautification of some proofs
Ning@localhost
parents: 21
diff changeset
    96
  then show "R b a" using ab unfolding SYM_def by blast
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
    97
qed
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
    98
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
    99
lemma R_trans2:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   100
  assumes ac: "R a c"
22
5023bf36d81a beautification of some proofs
Ning@localhost
parents: 21
diff changeset
   101
  and     bd: "R b d"
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   102
  shows "R a b = R c d"
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   103
proof
23
f6c6cf8c3b98 some more beautification
Ning@localhost
parents: 22
diff changeset
   104
  assume "R a b"
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   105
  then have "R b a" using R_sym by blast
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   106
  then have "R b c" using ac R_trans by blast
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   107
  then have "R c b" using R_sym by blast
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   108
  then show "R c d" using bd R_trans by blast
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   109
next
23
f6c6cf8c3b98 some more beautification
Ning@localhost
parents: 22
diff changeset
   110
  assume "R c d"
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   111
  then have "R a d" using ac R_trans by blast
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   112
  then have "R d a" using R_sym by blast
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   113
  then have "R b a" using bd R_trans by blast
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   114
  then show "R a b" using R_sym by blast
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   115
qed
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   116
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   117
lemma REPS_same:
25
9020ee23a020 The tactic with REPEAT, CHANGED and a proper simpset.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 24
diff changeset
   118
  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
   119
proof -
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   120
  have "R (REP a) (REP b) = (a = b)"
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   121
  proof
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   122
    assume as: "R (REP a) (REP b)"
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   123
    from rep_prop
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   124
    obtain x y
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   125
      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
   126
    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
   127
    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
   128
    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
   129
    then have "R y x" using lem9 by simp
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   130
    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
   131
    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
   132
    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
   133
    then show "a = b" using rep_inverse by simp
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   134
  next
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   135
    assume ab: "a = b"
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   136
    have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   137
    then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   138
  qed
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   139
  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
   140
qed
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   141
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   142
end
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   143
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   144
section {* type definition for the quotient type *}
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   145
71
35be65791f1d exported parts of QuotMain into a separate ML-file
Christian Urban <urbanc@in.tum.de>
parents: 70
diff changeset
   146
use "quotient.ML"
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   147
79
c0c41fefeb06 added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
parents: 77
diff changeset
   148
term EQUIV
c0c41fefeb06 added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
parents: 77
diff changeset
   149
14
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   150
ML {*
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   151
val no_vars = Thm.rule_attribute (fn context => fn th =>
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   152
  let
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   153
    val ctxt = Variable.set_body false (Context.proof_of context);
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   154
    val ((_, [th']), _) = Variable.import true [th] ctxt;
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   155
  in th' end);
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   156
*}
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   157
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   158
section {* various tests for quotient types*}
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   159
datatype trm =
15
f46eddb570a3 Cleaning the code
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 14
diff changeset
   160
  var  "nat"
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   161
| app  "trm" "trm"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   162
| lam  "nat" "trm"
13
c13bb9e02eb7 Fixes after suggestions from Makarius:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 12
diff changeset
   163
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   164
axiomatization
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   165
  RR :: "trm \<Rightarrow> trm \<Rightarrow> bool"
26
68d64432623e slight tuning
Christian Urban <urbanc@in.tum.de>
parents: 24
diff changeset
   166
where
14
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   167
  r_eq: "EQUIV RR"
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   168
81
c8d58e2cda58 slightly modified the parser
Christian Urban <urbanc@in.tum.de>
parents: 80
diff changeset
   169
quotient qtrm = trm / "RR"
79
c0c41fefeb06 added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
parents: 77
diff changeset
   170
  apply(rule r_eq)
c0c41fefeb06 added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
parents: 77
diff changeset
   171
  done
c0c41fefeb06 added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
parents: 77
diff changeset
   172
c0c41fefeb06 added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
parents: 77
diff changeset
   173
typ qtrm
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   174
term Rep_qtrm
2
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   175
term REP_qtrm
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   176
term Abs_qtrm
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   177
term ABS_qtrm
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   178
thm QUOT_TYPE_qtrm
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   179
thm QUOTIENT_qtrm
79
c0c41fefeb06 added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
parents: 77
diff changeset
   180
thm REP_qtrm_def
2
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   181
16
06b158ee1545 Code cleanup
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 15
diff changeset
   182
(* Test interpretation *)
06b158ee1545 Code cleanup
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 15
diff changeset
   183
thm QUOT_TYPE_I_qtrm.thm11
26
68d64432623e slight tuning
Christian Urban <urbanc@in.tum.de>
parents: 24
diff changeset
   184
thm QUOT_TYPE.thm11
16
06b158ee1545 Code cleanup
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 15
diff changeset
   185
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   186
print_theorems
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   187
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   188
thm Rep_qtrm
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   189
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   190
text {* another test *}
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   191
datatype 'a trm' =
15
f46eddb570a3 Cleaning the code
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 14
diff changeset
   192
  var'  "'a"
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   193
| app'  "'a trm'" "'a trm'"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   194
| lam'  "'a" "'a trm'"
15
f46eddb570a3 Cleaning the code
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 14
diff changeset
   195
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   196
consts R' :: "'a trm' \<Rightarrow> 'a trm' \<Rightarrow> bool"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   197
axioms r_eq': "EQUIV R'"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   198
81
c8d58e2cda58 slightly modified the parser
Christian Urban <urbanc@in.tum.de>
parents: 80
diff changeset
   199
quotient qtrm' = "'a trm'" / "R'"
79
c0c41fefeb06 added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
parents: 77
diff changeset
   200
  apply(rule r_eq')
c0c41fefeb06 added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
parents: 77
diff changeset
   201
  done
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   202
14
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   203
print_theorems
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   204
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   205
term ABS_qtrm'
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   206
term REP_qtrm'
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   207
thm QUOT_TYPE_qtrm'
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   208
thm QUOTIENT_qtrm'
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   209
thm Rep_qtrm'
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   210
14
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   211
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   212
text {* a test with lists of terms *}
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   213
datatype t =
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   214
  vr "string"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   215
| ap "t list"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   216
| lm "string" "t"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   217
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   218
consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   219
axioms t_eq: "EQUIV Rt"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   220
81
c8d58e2cda58 slightly modified the parser
Christian Urban <urbanc@in.tum.de>
parents: 80
diff changeset
   221
quotient qt = "t" / "Rt"
79
c0c41fefeb06 added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
parents: 77
diff changeset
   222
  by (rule t_eq)
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   223
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   224
section {* lifting of constants *}
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   225
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   226
text {* information about map-functions for type-constructor *}
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   227
ML {*
75
5fe163543bb8 started some strange functions
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   228
type typ_info = {mapfun: string, relfun: string}
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   229
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   230
local
59
1a92820a5b85 simplified the storage of the map-functions by using TheoryDataFun
Christian Urban <urbanc@in.tum.de>
parents: 58
diff changeset
   231
  structure Data = TheoryDataFun
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   232
  (type T = typ_info Symtab.table
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   233
   val empty = Symtab.empty
59
1a92820a5b85 simplified the storage of the map-functions by using TheoryDataFun
Christian Urban <urbanc@in.tum.de>
parents: 58
diff changeset
   234
   val copy = I
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   235
   val extend = I
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   236
   fun merge _ = Symtab.merge (K true))
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   237
in
46
e801b929216b some tuning of my code
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   238
  val lookup = Symtab.lookup o Data.get
e801b929216b some tuning of my code
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   239
  fun update k v = Data.map (Symtab.update (k, v))
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   240
end
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   241
*}
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   242
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   243
(* mapfuns for some standard types *)
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   244
setup {*
75
5fe163543bb8 started some strange functions
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   245
  update @{type_name "list"} {mapfun = @{const_name "map"},      relfun = @{const_name "LIST_REL"}} #> 
5fe163543bb8 started some strange functions
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   246
  update @{type_name "*"}    {mapfun = @{const_name "prod_fun"}, relfun = "???"} #> 
5fe163543bb8 started some strange functions
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   247
  update @{type_name "fun"}  {mapfun = @{const_name "fun_map"},  relfun = @{const_name "FUN_REL"}}
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   248
*}
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   249
59
1a92820a5b85 simplified the storage of the map-functions by using TheoryDataFun
Christian Urban <urbanc@in.tum.de>
parents: 58
diff changeset
   250
ML {* lookup @{theory} @{type_name list} *}
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   251
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   252
ML {*
46
e801b929216b some tuning of my code
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   253
datatype flag = absF | repF
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   254
46
e801b929216b some tuning of my code
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   255
fun get_fun flag rty qty lthy ty =
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   256
let
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   257
  val qty_name = Long_Name.base_name (fst (dest_Type qty))
15
f46eddb570a3 Cleaning the code
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 14
diff changeset
   258
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   259
  fun get_fun_aux s fs_tys =
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   260
  let
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   261
    val (fs, tys) = split_list fs_tys
15
f46eddb570a3 Cleaning the code
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 14
diff changeset
   262
    val (otys, ntys) = split_list tys
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   263
    val oty = Type (s, otys)
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   264
    val nty = Type (s, ntys)
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   265
    val ftys = map (op -->) tys
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   266
  in
59
1a92820a5b85 simplified the storage of the map-functions by using TheoryDataFun
Christian Urban <urbanc@in.tum.de>
parents: 58
diff changeset
   267
   (case (lookup (ProofContext.theory_of lthy) s) of
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   268
      SOME info => (list_comb (Const (#mapfun info, ftys ---> oty --> nty), fs), (oty, nty))
41
72d63aa8af68 added ctxt as explicit argument to build_goal; tuned
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   269
    | NONE      => raise ERROR ("no map association for type " ^ s))
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   270
  end
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   271
46
e801b929216b some tuning of my code
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   272
  fun get_const absF = (Const ("QuotMain.ABS_" ^ qty_name, rty --> qty), (rty, qty))
e801b929216b some tuning of my code
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   273
    | get_const repF = (Const ("QuotMain.REP_" ^ qty_name, qty --> rty), (qty, rty))
41
72d63aa8af68 added ctxt as explicit argument to build_goal; tuned
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   274
70
f3cbda066c3a consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   275
  fun mk_identity ty = Abs ("", ty, Bound 0)
41
72d63aa8af68 added ctxt as explicit argument to build_goal; tuned
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   276
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   277
in
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   278
  if ty = qty
46
e801b929216b some tuning of my code
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   279
  then (get_const flag)
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   280
  else (case ty of
41
72d63aa8af68 added ctxt as explicit argument to build_goal; tuned
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   281
          TFree _ => (mk_identity ty, (ty, ty))
72d63aa8af68 added ctxt as explicit argument to build_goal; tuned
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   282
        | Type (_, []) => (mk_identity ty, (ty, ty))
46
e801b929216b some tuning of my code
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   283
        | Type (s, tys) => get_fun_aux s (map (get_fun flag rty qty lthy) tys)
41
72d63aa8af68 added ctxt as explicit argument to build_goal; tuned
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   284
        | _ => raise ERROR ("no type variables")
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   285
       )
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   286
end
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   287
*}
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   288
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   289
ML {*
75
5fe163543bb8 started some strange functions
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   290
  get_fun repF @{typ t} @{typ qt} @{context} @{typ "((t \<Rightarrow> t) list) * nat"}
2
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   291
  |> fst
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   292
  |> Syntax.string_of_term @{context}
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   293
  |> writeln
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   294
*}
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   295
46
e801b929216b some tuning of my code
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   296
ML {*
e801b929216b some tuning of my code
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   297
  get_fun absF @{typ t} @{typ qt} @{context} @{typ "t * nat"}
e801b929216b some tuning of my code
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   298
  |> fst
e801b929216b some tuning of my code
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   299
  |> Syntax.string_of_term @{context}
e801b929216b some tuning of my code
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   300
  |> writeln
e801b929216b some tuning of my code
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   301
*}
2
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   302
76
1a0b771051c7 The tyREL function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 75
diff changeset
   303
ML {* op --> *}
1a0b771051c7 The tyREL function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 75
diff changeset
   304
ML {* op ---> *}
1a0b771051c7 The tyREL function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 75
diff changeset
   305
term FUN_REL
1a0b771051c7 The tyREL function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 75
diff changeset
   306
term LIST_REL
1a0b771051c7 The tyREL function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 75
diff changeset
   307
1a0b771051c7 The tyREL function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 75
diff changeset
   308
ML {* @{const_name "op ="} *}
75
5fe163543bb8 started some strange functions
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   309
ML {*
5fe163543bb8 started some strange functions
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   310
fun tyRel ty rty rel lthy =
76
1a0b771051c7 The tyREL function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 75
diff changeset
   311
  if ty = rty then rel
75
5fe163543bb8 started some strange functions
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   312
  else (case ty of
76
1a0b771051c7 The tyREL function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 75
diff changeset
   313
          Type (s, tys) =>
1a0b771051c7 The tyREL function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 75
diff changeset
   314
            let
1a0b771051c7 The tyREL function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 75
diff changeset
   315
              val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys;
1a0b771051c7 The tyREL function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 75
diff changeset
   316
              val ty_out = ty --> ty --> @{typ bool};
1a0b771051c7 The tyREL function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 75
diff changeset
   317
              val tys_out = tys_rel ---> ty_out;
1a0b771051c7 The tyREL function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 75
diff changeset
   318
            in
75
5fe163543bb8 started some strange functions
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   319
            (case (lookup (ProofContext.theory_of lthy) s) of
76
1a0b771051c7 The tyREL function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 75
diff changeset
   320
               SOME (info) => list_comb (Const (#relfun info, tys_out), map (fn ty => tyRel ty rty rel lthy) tys)
1a0b771051c7 The tyREL function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 75
diff changeset
   321
             | NONE  => Const (@{const_name "op ="}, ty --> ty --> @{typ bool})
75
5fe163543bb8 started some strange functions
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   322
            )
76
1a0b771051c7 The tyREL function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 75
diff changeset
   323
            end
1a0b771051c7 The tyREL function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 75
diff changeset
   324
        | _ => Const (@{const_name "op ="}, ty --> ty --> @{typ bool}))
75
5fe163543bb8 started some strange functions
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   325
*}
5fe163543bb8 started some strange functions
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   326
5fe163543bb8 started some strange functions
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   327
ML {*
76
1a0b771051c7 The tyREL function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 75
diff changeset
   328
  cterm_of @{theory} (tyRel @{typ "trm \<Rightarrow> bool"} @{typ "trm"} @{term "RR"} @{context})
1a0b771051c7 The tyREL function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 75
diff changeset
   329
*}
1a0b771051c7 The tyREL function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 75
diff changeset
   330
1a0b771051c7 The tyREL function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 75
diff changeset
   331
(* ML {*
75
5fe163543bb8 started some strange functions
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   332
5fe163543bb8 started some strange functions
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   333
fun regularise trm \<Rightarrow> new_trm 
5fe163543bb8 started some strange functions
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   334
  (case trm of
5fe163543bb8 started some strange functions
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   335
     ??
5fe163543bb8 started some strange functions
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   336
  )
5fe163543bb8 started some strange functions
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   337
*}
5fe163543bb8 started some strange functions
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   338
5fe163543bb8 started some strange functions
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   339
fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this)
5fe163543bb8 started some strange functions
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   340
  trm == new_trm
5fe163543bb8 started some strange functions
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   341
*)
5fe163543bb8 started some strange functions
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   342
41
72d63aa8af68 added ctxt as explicit argument to build_goal; tuned
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   343
text {* produces the definition for a lifted constant *}
2
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   344
ML {*
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   345
fun get_const_def nconst oconst rty qty lthy =
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   346
let
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   347
  val ty = fastype_of nconst
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   348
  val (arg_tys, res_ty) = strip_type ty
14
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   349
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   350
  val fresh_args = arg_tys |> map (pair "x")
15
f46eddb570a3 Cleaning the code
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 14
diff changeset
   351
                           |> Variable.variant_frees lthy [nconst, oconst]
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   352
                           |> map Free
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   353
46
e801b929216b some tuning of my code
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   354
  val rep_fns = map (fst o get_fun repF rty qty lthy) arg_tys
e801b929216b some tuning of my code
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   355
  val abs_fn  = (fst o get_fun absF rty qty lthy) res_ty
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   356
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   357
in
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   358
  map (op $) (rep_fns ~~ fresh_args)
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   359
  |> curry list_comb oconst
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   360
  |> curry (op $) abs_fn
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   361
  |> fold_rev lambda fresh_args
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   362
end
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   363
*}
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   364
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   365
ML {*
15
f46eddb570a3 Cleaning the code
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 14
diff changeset
   366
fun exchange_ty rty qty ty =
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   367
  if ty = rty
41
72d63aa8af68 added ctxt as explicit argument to build_goal; tuned
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   368
  then qty
15
f46eddb570a3 Cleaning the code
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 14
diff changeset
   369
  else
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   370
    (case ty of
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   371
       Type (s, tys) => Type (s, map (exchange_ty rty qty) tys)
41
72d63aa8af68 added ctxt as explicit argument to build_goal; tuned
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   372
      | _ => ty
72d63aa8af68 added ctxt as explicit argument to build_goal; tuned
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   373
    )
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   374
*}
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   375
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   376
ML {*
17
55b646c6c4cd More naming/binding suggestions from Makarius
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 16
diff changeset
   377
fun make_const_def nconst_bname oconst mx rty qty lthy =
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   378
let
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   379
  val oconst_ty = fastype_of oconst
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   380
  val nconst_ty = exchange_ty rty qty oconst_ty
17
55b646c6c4cd More naming/binding suggestions from Makarius
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 16
diff changeset
   381
  val nconst = Const (Binding.name_of nconst_bname, nconst_ty)
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   382
  val def_trm = get_const_def nconst oconst rty qty lthy
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   383
in
79
c0c41fefeb06 added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
parents: 77
diff changeset
   384
  define (nconst_bname, mx, def_trm) lthy
15
f46eddb570a3 Cleaning the code
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 14
diff changeset
   385
end
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   386
*}
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   387
2
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   388
local_setup {*
41
72d63aa8af68 added ctxt as explicit argument to build_goal; tuned
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   389
  make_const_def @{binding VR} @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd #>
72d63aa8af68 added ctxt as explicit argument to build_goal; tuned
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   390
  make_const_def @{binding AP} @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd #>
17
55b646c6c4cd More naming/binding suggestions from Makarius
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 16
diff changeset
   391
  make_const_def @{binding LM} @{term "lm"} NoSyn @{typ "t"} @{typ "qt"} #> snd
2
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   392
*}
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   393
41
72d63aa8af68 added ctxt as explicit argument to build_goal; tuned
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   394
term vr
72d63aa8af68 added ctxt as explicit argument to build_goal; tuned
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   395
term ap
72d63aa8af68 added ctxt as explicit argument to build_goal; tuned
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   396
term lm
72d63aa8af68 added ctxt as explicit argument to build_goal; tuned
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   397
thm VR_def AP_def LM_def
14
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   398
term LM
2
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   399
term VR
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   400
term AP
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   401
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   402
text {* a test with functions *}
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   403
datatype 'a t' =
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   404
  vr' "string"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   405
| ap' "('a t') * ('a t')"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   406
| lm' "'a" "string \<Rightarrow> ('a t')"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   407
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   408
consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   409
axioms t_eq': "EQUIV Rt'"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   410
81
c8d58e2cda58 slightly modified the parser
Christian Urban <urbanc@in.tum.de>
parents: 80
diff changeset
   411
quotient qt' = "'a t'" / "Rt'"
79
c0c41fefeb06 added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
parents: 77
diff changeset
   412
  apply(rule t_eq')
c0c41fefeb06 added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
parents: 77
diff changeset
   413
  done
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   414
14
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   415
print_theorems
2
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   416
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   417
local_setup {*
41
72d63aa8af68 added ctxt as explicit argument to build_goal; tuned
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   418
  make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #>
72d63aa8af68 added ctxt as explicit argument to build_goal; tuned
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   419
  make_const_def @{binding AP'} @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #>
17
55b646c6c4cd More naming/binding suggestions from Makarius
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 16
diff changeset
   420
  make_const_def @{binding LM'} @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   421
*}
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   422
41
72d63aa8af68 added ctxt as explicit argument to build_goal; tuned
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   423
term vr'
72d63aa8af68 added ctxt as explicit argument to build_goal; tuned
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   424
term ap'
72d63aa8af68 added ctxt as explicit argument to build_goal; tuned
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   425
term ap'
72d63aa8af68 added ctxt as explicit argument to build_goal; tuned
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   426
thm VR'_def AP'_def LM'_def
14
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   427
term LM'
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   428
term VR'
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   429
term AP'
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   430
14
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   431
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   432
text {* finite set example *}
13
c13bb9e02eb7 Fixes after suggestions from Makarius:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 12
diff changeset
   433
print_syntax
14
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   434
inductive
13
c13bb9e02eb7 Fixes after suggestions from Makarius:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 12
diff changeset
   435
  list_eq (infix "\<approx>" 50)
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   436
where
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   437
  "a#b#xs \<approx> b#a#xs"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   438
| "[] \<approx> []"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   439
| "xs \<approx> ys \<Longrightarrow> ys \<approx> xs"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   440
| "a#a#xs \<approx> a#xs"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   441
| "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   442
| "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   443
47
6a51704204e5 consistent state
Christian Urban <urbanc@in.tum.de>
parents: 46
diff changeset
   444
lemma list_eq_refl:
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   445
  shows "xs \<approx> xs"
13
c13bb9e02eb7 Fixes after suggestions from Makarius:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 12
diff changeset
   446
  apply (induct xs)
c13bb9e02eb7 Fixes after suggestions from Makarius:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 12
diff changeset
   447
   apply (auto intro: list_eq.intros)
c13bb9e02eb7 Fixes after suggestions from Makarius:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 12
diff changeset
   448
  done
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   449
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   450
lemma equiv_list_eq:
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   451
  shows "EQUIV list_eq"
13
c13bb9e02eb7 Fixes after suggestions from Makarius:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 12
diff changeset
   452
  unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def
47
6a51704204e5 consistent state
Christian Urban <urbanc@in.tum.de>
parents: 46
diff changeset
   453
  apply(auto intro: list_eq.intros list_eq_refl)
13
c13bb9e02eb7 Fixes after suggestions from Makarius:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 12
diff changeset
   454
  done
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   455
81
c8d58e2cda58 slightly modified the parser
Christian Urban <urbanc@in.tum.de>
parents: 80
diff changeset
   456
quotient fset = "'a list" / "list_eq"
79
c0c41fefeb06 added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
parents: 77
diff changeset
   457
  apply(rule equiv_list_eq)
c0c41fefeb06 added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
parents: 77
diff changeset
   458
  done
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   459
14
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   460
print_theorems
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   461
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   462
typ "'a fset"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   463
thm "Rep_fset"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   464
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   465
local_setup {*
17
55b646c6c4cd More naming/binding suggestions from Makarius
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 16
diff changeset
   466
  make_const_def @{binding EMPTY} @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   467
*}
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   468
14
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   469
term Nil
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   470
term EMPTY
2
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   471
thm EMPTY_def
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   472
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   473
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   474
local_setup {*
17
55b646c6c4cd More naming/binding suggestions from Makarius
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 16
diff changeset
   475
  make_const_def @{binding INSERT} @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   476
*}
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   477
14
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   478
term Cons
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   479
term INSERT
2
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   480
thm INSERT_def
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   481
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   482
local_setup {*
17
55b646c6c4cd More naming/binding suggestions from Makarius
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 16
diff changeset
   483
  make_const_def @{binding UNION} @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   484
*}
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   485
15
f46eddb570a3 Cleaning the code
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 14
diff changeset
   486
term append
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   487
term UNION
2
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   488
thm UNION_def
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   489
7
3e77ad0abc6a - Build an interpretation for fset from ML level and use it
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 6
diff changeset
   490
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   491
thm QUOTIENT_fset
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   492
14
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   493
thm QUOT_TYPE_I_fset.thm11
9
eac147a5eb33 Changed to the use of "modern interface"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 8
diff changeset
   494
eac147a5eb33 Changed to the use of "modern interface"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 8
diff changeset
   495
13
c13bb9e02eb7 Fixes after suggestions from Makarius:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 12
diff changeset
   496
fun
c13bb9e02eb7 Fixes after suggestions from Makarius:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 12
diff changeset
   497
  membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infix "memb" 100)
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   498
where
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   499
  m1: "(x memb []) = False"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   500
| m2: "(x memb (y#xs)) = ((x=y) \<or> (x memb xs))"
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   501
2
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   502
lemma mem_respects:
9
eac147a5eb33 Changed to the use of "modern interface"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 8
diff changeset
   503
  fixes z
2
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   504
  assumes a: "list_eq x y"
9
eac147a5eb33 Changed to the use of "modern interface"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 8
diff changeset
   505
  shows "(z memb x) = (z memb y)"
13
c13bb9e02eb7 Fixes after suggestions from Makarius:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 12
diff changeset
   506
  using a by induct auto
c13bb9e02eb7 Fixes after suggestions from Makarius:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 12
diff changeset
   507
2
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   508
29
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   509
fun
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   510
  card1 :: "'a list \<Rightarrow> nat"
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   511
where
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   512
  card1_nil: "(card1 []) = 0"
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   513
| card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))"
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   514
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   515
local_setup {*
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   516
  make_const_def @{binding card} @{term "card1"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   517
*}
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   518
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   519
term card1
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   520
term card
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   521
thm card_def
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   522
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   523
(* text {*
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   524
 Maybe make_const_def should require a theorem that says that the particular lifted function
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   525
 respects the relation. With it such a definition would be impossible:
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   526
 make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
41
72d63aa8af68 added ctxt as explicit argument to build_goal; tuned
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   527
*}*)
29
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   528
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   529
lemma card1_rsp:
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   530
  fixes a b :: "'a list"
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   531
  assumes e: "a \<approx> b"
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   532
  shows "card1 a = card1 b"
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   533
  using e apply induct
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   534
  apply (simp_all add:mem_respects)
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   535
  done
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   536
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   537
lemma card1_0:
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   538
  fixes a :: "'a list"
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   539
  shows "(card1 a = 0) = (a = [])"
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   540
  apply (induct a)
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   541
   apply (simp)
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   542
  apply (simp_all)
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   543
   apply meson
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   544
  apply (simp_all)
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   545
  done
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   546
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   547
lemma not_mem_card1:
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   548
  fixes x :: "'a"
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   549
  fixes xs :: "'a list"
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   550
  shows "~(x memb xs) \<Longrightarrow> card1 (x # xs) = Suc (card1 xs)"
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   551
  by simp
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   552
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   553
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   554
lemma mem_cons:
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   555
  fixes x :: "'a"
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   556
  fixes xs :: "'a list"
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   557
  assumes a : "x memb xs"
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   558
  shows "x # xs \<approx> xs"
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   559
  using a
38
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   560
  apply (induct xs)
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   561
  apply (auto intro: list_eq.intros)
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   562
  done
29
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   563
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   564
lemma card1_suc:
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   565
  fixes xs :: "'a list"
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   566
  fixes n :: "nat"
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   567
  assumes c: "card1 xs = Suc n"
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   568
  shows "\<exists>a ys. ~(a memb ys) \<and> xs \<approx> (a # ys)"
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   569
  using c
38
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   570
apply(induct xs)
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   571
apply (metis Suc_neq_Zero card1_0)
47
6a51704204e5 consistent state
Christian Urban <urbanc@in.tum.de>
parents: 46
diff changeset
   572
apply (metis QUOT_TYPE_I_fset.R_trans QuotMain.card1_cons list_eq_refl mem_cons)
38
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   573
done
29
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   574
12
13b527da2157 More examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 11
diff changeset
   575
lemma cons_preserves:
13b527da2157 More examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 11
diff changeset
   576
  fixes z
13b527da2157 More examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 11
diff changeset
   577
  assumes a: "xs \<approx> ys"
13b527da2157 More examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 11
diff changeset
   578
  shows "(z # xs) \<approx> (z # ys)"
13
c13bb9e02eb7 Fixes after suggestions from Makarius:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 12
diff changeset
   579
  using a by (rule QuotMain.list_eq.intros(5))
12
13b527da2157 More examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 11
diff changeset
   580
60
4826ad24f772 First theorem with quantifiers. Learned how to use sledgehammer.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 58
diff changeset
   581
lemma fs1_strong_cases:
4826ad24f772 First theorem with quantifiers. Learned how to use sledgehammer.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 58
diff changeset
   582
  fixes X :: "'a list"
4826ad24f772 First theorem with quantifiers. Learned how to use sledgehammer.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 58
diff changeset
   583
  shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a memb Y) \<and> (X \<approx> a # Y)))"
4826ad24f772 First theorem with quantifiers. Learned how to use sledgehammer.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 58
diff changeset
   584
  apply (induct X)
4826ad24f772 First theorem with quantifiers. Learned how to use sledgehammer.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 58
diff changeset
   585
  apply (simp)
72
4efc9e6661a4 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 71
diff changeset
   586
  apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons QuotMain.m1)
60
4826ad24f772 First theorem with quantifiers. Learned how to use sledgehammer.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 58
diff changeset
   587
  done
29
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   588
72
4efc9e6661a4 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 71
diff changeset
   589
29
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   590
text {*
68
e8660818c755 renamed unlam_def to unabs_def (matching the function abs_def in drule.ML)
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   591
  Unabs_def converts a definition given as
40
c8187c293587 slightly tuned the comment for unlam
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   592
c8187c293587 slightly tuned the comment for unlam
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   593
    c \<equiv> %x. %y. f x y
c8187c293587 slightly tuned the comment for unlam
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   594
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   595
  to a theorem of the form
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   596
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   597
    c x y \<equiv> f x y
40
c8187c293587 slightly tuned the comment for unlam
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   598
c8187c293587 slightly tuned the comment for unlam
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   599
  This function is needed to rewrite the right-hand
c8187c293587 slightly tuned the comment for unlam
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   600
  side to the left-hand side.
29
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   601
*}
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   602
11
0bc0db2e83f2 Use metavariables in the 'non-lambda' definitions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 10
diff changeset
   603
ML {*
68
e8660818c755 renamed unlam_def to unabs_def (matching the function abs_def in drule.ML)
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   604
fun unabs_def ctxt def =
64
33d7bcfd5603 simplified the unlam_def function
Christian Urban <urbanc@in.tum.de>
parents: 63
diff changeset
   605
let
33d7bcfd5603 simplified the unlam_def function
Christian Urban <urbanc@in.tum.de>
parents: 63
diff changeset
   606
  val (lhs, rhs) = Thm.dest_equals (cprop_of def)
33d7bcfd5603 simplified the unlam_def function
Christian Urban <urbanc@in.tum.de>
parents: 63
diff changeset
   607
  val xs = strip_abs_vars (term_of rhs)
33d7bcfd5603 simplified the unlam_def function
Christian Urban <urbanc@in.tum.de>
parents: 63
diff changeset
   608
  val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt
65
da982cded326 one further improvement to unlam_def
Christian Urban <urbanc@in.tum.de>
parents: 64
diff changeset
   609
  
da982cded326 one further improvement to unlam_def
Christian Urban <urbanc@in.tum.de>
parents: 64
diff changeset
   610
  val thy = ProofContext.theory_of ctxt'
66
564bf4343f63 another improvement to unlam_def
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   611
  val cxs = map (cterm_of thy o Free) xs
564bf4343f63 another improvement to unlam_def
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   612
  val new_lhs = Drule.list_comb (lhs, cxs)
64
33d7bcfd5603 simplified the unlam_def function
Christian Urban <urbanc@in.tum.de>
parents: 63
diff changeset
   613
33d7bcfd5603 simplified the unlam_def function
Christian Urban <urbanc@in.tum.de>
parents: 63
diff changeset
   614
  fun get_conv [] = Conv.rewr_conv def
33d7bcfd5603 simplified the unlam_def function
Christian Urban <urbanc@in.tum.de>
parents: 63
diff changeset
   615
    | get_conv (x::xs) = Conv.fun_conv (get_conv xs)
33d7bcfd5603 simplified the unlam_def function
Christian Urban <urbanc@in.tum.de>
parents: 63
diff changeset
   616
in
66
564bf4343f63 another improvement to unlam_def
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   617
  get_conv xs new_lhs |>  
64
33d7bcfd5603 simplified the unlam_def function
Christian Urban <urbanc@in.tum.de>
parents: 63
diff changeset
   618
  singleton (ProofContext.export ctxt' ctxt)
33d7bcfd5603 simplified the unlam_def function
Christian Urban <urbanc@in.tum.de>
parents: 63
diff changeset
   619
end
10
b11b405b8271 Make both kinds of definitions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 9
diff changeset
   620
*}
9
eac147a5eb33 Changed to the use of "modern interface"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 8
diff changeset
   621
10
b11b405b8271 Make both kinds of definitions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 9
diff changeset
   622
local_setup {*
17
55b646c6c4cd More naming/binding suggestions from Makarius
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 16
diff changeset
   623
  make_const_def @{binding IN} @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
10
b11b405b8271 Make both kinds of definitions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 9
diff changeset
   624
*}
b11b405b8271 Make both kinds of definitions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 9
diff changeset
   625
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   626
term membship
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   627
term IN
2
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   628
thm IN_def
66
564bf4343f63 another improvement to unlam_def
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   629
68
e8660818c755 renamed unlam_def to unabs_def (matching the function abs_def in drule.ML)
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   630
(* unabs_def tests *)
67
221e926da073 tuned; nothing serious
Christian Urban <urbanc@in.tum.de>
parents: 66
diff changeset
   631
ML {* (Conv.fun_conv (Conv.fun_conv (Conv.rewr_conv @{thm IN_def}))) @{cterm "IN x y"} *}
64
33d7bcfd5603 simplified the unlam_def function
Christian Urban <urbanc@in.tum.de>
parents: 63
diff changeset
   632
ML {* MetaSimplifier.rewrite_rule @{thms IN_def} @{thm IN_def}*}
68
e8660818c755 renamed unlam_def to unabs_def (matching the function abs_def in drule.ML)
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   633
ML {* @{thm IN_def}; unabs_def @{context} @{thm IN_def} *}
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   634
2
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   635
lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset]
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   636
thm QUOT_TYPE.thm11[OF QUOT_TYPE_fset, THEN iffD1, simplified a]
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   637
2
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   638
lemma yy:
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   639
  shows "(False = x memb []) = (False = IN (x::nat) EMPTY)"
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   640
unfolding IN_def EMPTY_def
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   641
apply(rule_tac f="(op =) False" in arg_cong)
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   642
apply(rule mem_respects)
14
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   643
apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
2
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   644
apply(rule list_eq.intros)
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   645
done
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   646
2
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   647
lemma
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   648
  shows "IN (x::nat) EMPTY = False"
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   649
using m1
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   650
apply -
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   651
apply(rule yy[THEN iffD1, symmetric])
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   652
apply(simp)
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   653
done
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   654
2
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   655
lemma
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   656
  shows "((x=y) \<or> (IN x xs) = (IN (x::nat) (INSERT y xs))) =
23
f6c6cf8c3b98 some more beautification
Ning@localhost
parents: 22
diff changeset
   657
         ((x=y) \<or> x memb REP_fset xs = x memb (y # REP_fset xs))"
2
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   658
unfolding IN_def INSERT_def
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   659
apply(rule_tac f="(op \<or>) (x=y)" in arg_cong)
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   660
apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong)
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   661
apply(rule mem_respects)
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   662
apply(rule list_eq.intros(3))
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   663
apply(unfold REP_fset_def ABS_fset_def)
5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 4
diff changeset
   664
apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])
47
6a51704204e5 consistent state
Christian Urban <urbanc@in.tum.de>
parents: 46
diff changeset
   665
apply(rule list_eq_refl)
2
Christian Urban <urbanc@in.tum.de>
parents: 1
diff changeset
   666
done
0
ebe0ea8fe247 initial commit
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   667
7
3e77ad0abc6a - Build an interpretation for fset from ML level and use it
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 6
diff changeset
   668
lemma append_respects_fst:
14
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   669
  assumes a : "list_eq l1 l2"
4
Christian Urban <urbanc@in.tum.de>
parents: 3
diff changeset
   670
  shows "list_eq (l1 @ s) (l2 @ s)"
3
672e14609e6e UNION - Append theorem
cek@localhost.localdomain
parents: 2
diff changeset
   671
  using a
672e14609e6e UNION - Append theorem
cek@localhost.localdomain
parents: 2
diff changeset
   672
  apply(induct)
4
Christian Urban <urbanc@in.tum.de>
parents: 3
diff changeset
   673
  apply(auto intro: list_eq.intros)
47
6a51704204e5 consistent state
Christian Urban <urbanc@in.tum.de>
parents: 46
diff changeset
   674
  apply(simp add: list_eq_refl)
3
672e14609e6e UNION - Append theorem
cek@localhost.localdomain
parents: 2
diff changeset
   675
done
672e14609e6e UNION - Append theorem
cek@localhost.localdomain
parents: 2
diff changeset
   676
18
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   677
lemma yyy:
3
672e14609e6e UNION - Append theorem
cek@localhost.localdomain
parents: 2
diff changeset
   678
  shows "
672e14609e6e UNION - Append theorem
cek@localhost.localdomain
parents: 2
diff changeset
   679
    (
672e14609e6e UNION - Append theorem
cek@localhost.localdomain
parents: 2
diff changeset
   680
     (UNION EMPTY s = s) &
672e14609e6e UNION - Append theorem
cek@localhost.localdomain
parents: 2
diff changeset
   681
     ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))
672e14609e6e UNION - Append theorem
cek@localhost.localdomain
parents: 2
diff changeset
   682
    ) = (
672e14609e6e UNION - Append theorem
cek@localhost.localdomain
parents: 2
diff changeset
   683
     ((ABS_fset ([] @ REP_fset s)) = s) &
672e14609e6e UNION - Append theorem
cek@localhost.localdomain
parents: 2
diff changeset
   684
     ((ABS_fset ((e # (REP_fset s1)) @ REP_fset s2)) = ABS_fset (e # (REP_fset s1 @ REP_fset s2)))
672e14609e6e UNION - Append theorem
cek@localhost.localdomain
parents: 2
diff changeset
   685
    )"
672e14609e6e UNION - Append theorem
cek@localhost.localdomain
parents: 2
diff changeset
   686
  unfolding UNION_def EMPTY_def INSERT_def
672e14609e6e UNION - Append theorem
cek@localhost.localdomain
parents: 2
diff changeset
   687
  apply(rule_tac f="(op &)" in arg_cong2)
672e14609e6e UNION - Append theorem
cek@localhost.localdomain
parents: 2
diff changeset
   688
  apply(rule_tac f="(op =)" in arg_cong2)
14
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   689
  apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
7
3e77ad0abc6a - Build an interpretation for fset from ML level and use it
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 6
diff changeset
   690
  apply(rule append_respects_fst)
18
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   691
  apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
47
6a51704204e5 consistent state
Christian Urban <urbanc@in.tum.de>
parents: 46
diff changeset
   692
  apply(rule list_eq_refl)
3
672e14609e6e UNION - Append theorem
cek@localhost.localdomain
parents: 2
diff changeset
   693
  apply(simp)
672e14609e6e UNION - Append theorem
cek@localhost.localdomain
parents: 2
diff changeset
   694
  apply(rule_tac f="(op =)" in arg_cong2)
14
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   695
  apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
7
3e77ad0abc6a - Build an interpretation for fset from ML level and use it
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 6
diff changeset
   696
  apply(rule append_respects_fst)
14
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   697
  apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
47
6a51704204e5 consistent state
Christian Urban <urbanc@in.tum.de>
parents: 46
diff changeset
   698
  apply(rule list_eq_refl)
14
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   699
  apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
3
672e14609e6e UNION - Append theorem
cek@localhost.localdomain
parents: 2
diff changeset
   700
  apply(rule list_eq.intros(5))
14
5f6ee943c697 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 13
diff changeset
   701
  apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
47
6a51704204e5 consistent state
Christian Urban <urbanc@in.tum.de>
parents: 46
diff changeset
   702
  apply(rule list_eq_refl)
3
672e14609e6e UNION - Append theorem
cek@localhost.localdomain
parents: 2
diff changeset
   703
done
672e14609e6e UNION - Append theorem
cek@localhost.localdomain
parents: 2
diff changeset
   704
672e14609e6e UNION - Append theorem
cek@localhost.localdomain
parents: 2
diff changeset
   705
lemma
672e14609e6e UNION - Append theorem
cek@localhost.localdomain
parents: 2
diff changeset
   706
  shows "
672e14609e6e UNION - Append theorem
cek@localhost.localdomain
parents: 2
diff changeset
   707
     (UNION EMPTY s = s) &
7
3e77ad0abc6a - Build an interpretation for fset from ML level and use it
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 6
diff changeset
   708
     ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))"
3e77ad0abc6a - Build an interpretation for fset from ML level and use it
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 6
diff changeset
   709
  apply (simp add: yyy)
24
6885fa184e89 Merged with my changes from the morning:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 23
diff changeset
   710
  apply (simp add: QUOT_TYPE_I_fset.thm10)
7
3e77ad0abc6a - Build an interpretation for fset from ML level and use it
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 6
diff changeset
   711
  done
3
672e14609e6e UNION - Append theorem
cek@localhost.localdomain
parents: 2
diff changeset
   712
8
54afbcf2a758 Initial version of the function that builds goals.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 7
diff changeset
   713
ML {*
55
b2ab3ba388a0 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 54
diff changeset
   714
  fun mk_rep x = @{term REP_fset} $ x;
b2ab3ba388a0 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 54
diff changeset
   715
  fun mk_abs x = @{term ABS_fset} $ x;
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   716
  val consts = [@{const_name "Nil"}, @{const_name "append"},
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   717
                @{const_name "Cons"}, @{const_name "membship"},
41
72d63aa8af68 added ctxt as explicit argument to build_goal; tuned
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   718
                @{const_name "card1"}]
8
54afbcf2a758 Initial version of the function that builds goals.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 7
diff changeset
   719
*}
54afbcf2a758 Initial version of the function that builds goals.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 7
diff changeset
   720
56
ec5fbe7ab427 First version of handling of the universal quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 55
diff changeset
   721
ML {* val qty = @{typ "'a fset"} *}
ec5fbe7ab427 First version of handling of the universal quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 55
diff changeset
   722
ML {* val tt = Type ("fun", [Type ("fun", [qty, @{typ "prop"}]), @{typ "prop"}]) *}
58
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
   723
ML {* val fall = Const(@{const_name all}, dummyT) *}
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
   724
8
54afbcf2a758 Initial version of the function that builds goals.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 7
diff changeset
   725
ML {*
58
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
   726
fun build_goal_term ctxt thm constructors rty qty mk_rep mk_abs =
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   727
  let
55
b2ab3ba388a0 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 54
diff changeset
   728
    fun mk_rep_abs x = mk_rep (mk_abs x);
b2ab3ba388a0 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 54
diff changeset
   729
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   730
    fun is_constructor (Const (x, _)) = member (op =) constructors x
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   731
      | is_constructor _ = false;
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   732
43
e51af8bace65 Cleaning the code with Makarius
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 42
diff changeset
   733
    fun maybe_mk_rep_abs t =
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   734
      let
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   735
        val _ = writeln ("Maybe: " ^ Syntax.string_of_term ctxt t)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   736
      in
55
b2ab3ba388a0 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 54
diff changeset
   737
        if fastype_of t = rty then mk_rep_abs t else t
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   738
      end;
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   739
56
ec5fbe7ab427 First version of handling of the universal quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 55
diff changeset
   740
    fun is_all (Const ("all", Type("fun", [Type("fun", [ty, _]), _]))) = ty = rty
ec5fbe7ab427 First version of handling of the universal quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 55
diff changeset
   741
      | is_all _ = false;
ec5fbe7ab427 First version of handling of the universal quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 55
diff changeset
   742
58
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
   743
    fun is_ex (Const ("Ex", Type("fun", [Type("fun", [ty, _]), _]))) = ty = rty
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
   744
      | is_ex _ = false;
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
   745
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   746
    fun build_aux ctxt1 tm =
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   747
      let
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   748
        val (head, args) = Term.strip_comb tm;
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   749
        val args' = map (build_aux ctxt1) args;
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   750
      in
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   751
        (case head of
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   752
          Abs (x, T, t) =>
55
b2ab3ba388a0 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 54
diff changeset
   753
            if T = rty then let
b2ab3ba388a0 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 54
diff changeset
   754
              val ([x'], ctxt2) = Variable.variant_fixes [x] ctxt1;
b2ab3ba388a0 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 54
diff changeset
   755
              val v = Free (x', qty);
b2ab3ba388a0 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 54
diff changeset
   756
              val t' = subst_bound (mk_rep v, t);
b2ab3ba388a0 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 54
diff changeset
   757
              val rec_term = build_aux ctxt2 t';
b2ab3ba388a0 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 54
diff changeset
   758
              val _ = tracing (Syntax.string_of_term ctxt2 t')
b2ab3ba388a0 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 54
diff changeset
   759
              val _ = tracing (Syntax.string_of_term ctxt2 (Term.lambda_name (x, v) rec_term))
b2ab3ba388a0 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 54
diff changeset
   760
            in
b2ab3ba388a0 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 54
diff changeset
   761
              Term.lambda_name (x, v) rec_term
b2ab3ba388a0 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 54
diff changeset
   762
            end else let
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   763
              val ([x'], ctxt2) = Variable.variant_fixes [x] ctxt1;
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   764
              val v = Free (x', T);
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   765
              val t' = subst_bound (v, t);
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   766
              val rec_term = build_aux ctxt2 t';
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   767
            in Term.lambda_name (x, v) rec_term end
58
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
   768
        | _ =>  (* I assume that we never lift 'prop' since it is not of sort type *)
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
   769
            if is_all head then
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
   770
              list_comb (Const(@{const_name all}, dummyT), args') |> Syntax.check_term ctxt1
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
   771
            else if is_ex head then
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
   772
              list_comb (Const(@{const_name Ex}, dummyT), args') |> Syntax.check_term ctxt1
56
ec5fbe7ab427 First version of handling of the universal quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 55
diff changeset
   773
            else if is_constructor head then
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   774
              maybe_mk_rep_abs (list_comb (head, map maybe_mk_rep_abs args'))
56
ec5fbe7ab427 First version of handling of the universal quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 55
diff changeset
   775
            else
ec5fbe7ab427 First version of handling of the universal quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 55
diff changeset
   776
              maybe_mk_rep_abs (list_comb (head, args'))
ec5fbe7ab427 First version of handling of the universal quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 55
diff changeset
   777
        )
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   778
      end;
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   779
  in
58
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
   780
    build_aux ctxt (Thm.prop_of thm)
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   781
  end
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   782
*}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   783
58
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
   784
ML {*
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
   785
fun build_goal ctxt thm cons rty qty mk_rep mk_abs =
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
   786
  Logic.mk_equals ((build_goal_term ctxt thm cons rty qty mk_rep mk_abs), (Thm.prop_of thm))
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
   787
*}
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
   788
67
221e926da073 tuned; nothing serious
Christian Urban <urbanc@in.tum.de>
parents: 66
diff changeset
   789
ML {*
221e926da073 tuned; nothing serious
Christian Urban <urbanc@in.tum.de>
parents: 66
diff changeset
   790
  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))
221e926da073 tuned; nothing serious
Christian Urban <urbanc@in.tum.de>
parents: 66
diff changeset
   791
*}
221e926da073 tuned; nothing serious
Christian Urban <urbanc@in.tum.de>
parents: 66
diff changeset
   792
  
221e926da073 tuned; nothing serious
Christian Urban <urbanc@in.tum.de>
parents: 66
diff changeset
   793
ML {*
221e926da073 tuned; nothing serious
Christian Urban <urbanc@in.tum.de>
parents: 66
diff changeset
   794
m1_novars |> prop_of
221e926da073 tuned; nothing serious
Christian Urban <urbanc@in.tum.de>
parents: 66
diff changeset
   795
|> Syntax.string_of_term @{context}
221e926da073 tuned; nothing serious
Christian Urban <urbanc@in.tum.de>
parents: 66
diff changeset
   796
|> writeln; 
221e926da073 tuned; nothing serious
Christian Urban <urbanc@in.tum.de>
parents: 66
diff changeset
   797
build_goal_term @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
221e926da073 tuned; nothing serious
Christian Urban <urbanc@in.tum.de>
parents: 66
diff changeset
   798
|> Syntax.string_of_term @{context}
221e926da073 tuned; nothing serious
Christian Urban <urbanc@in.tum.de>
parents: 66
diff changeset
   799
|> writeln
221e926da073 tuned; nothing serious
Christian Urban <urbanc@in.tum.de>
parents: 66
diff changeset
   800
*}
221e926da073 tuned; nothing serious
Christian Urban <urbanc@in.tum.de>
parents: 66
diff changeset
   801
58
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
   802
29
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   803
ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}
68
e8660818c755 renamed unlam_def to unabs_def (matching the function abs_def in drule.ML)
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   804
ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *}
18
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   805
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   806
ML {*
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   807
  fun dest_cbinop t =
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   808
    let
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   809
      val (t2, rhs) = Thm.dest_comb t;
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   810
      val (bop, lhs) = Thm.dest_comb t2;
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   811
    in
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   812
      (bop, (lhs, rhs))
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   813
    end
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   814
*}
38
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   815
18
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   816
ML {*
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   817
  fun dest_ceq t =
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   818
    let
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   819
      val (bop, pair) = dest_cbinop t;
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   820
      val (bop_s, _) = Term.dest_Const (Thm.term_of bop);
18
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   821
    in
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   822
      if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t]))
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   823
    end
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   824
*}
38
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
   825
19
55aefc2d524a The tactic still only for fset
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 18
diff changeset
   826
ML Thm.instantiate
55aefc2d524a The tactic still only for fset
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 18
diff changeset
   827
ML {*@{thm arg_cong2}*}
55aefc2d524a The tactic still only for fset
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 18
diff changeset
   828
ML {*@{thm arg_cong2[of _ _ _ _ "op ="]} *}
55aefc2d524a The tactic still only for fset
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 18
diff changeset
   829
ML {* val cT = @{cpat "op ="} |> Thm.ctyp_of_term |> Thm.dest_ctyp |> hd *}
25
9020ee23a020 The tactic with REPEAT, CHANGED and a proper simpset.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 24
diff changeset
   830
ML {*
19
55aefc2d524a The tactic still only for fset
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 18
diff changeset
   831
  Toplevel.program (fn () =>
50
18d8bcd769b3 Checked again with the version on my hard-drive backedup yesterday and fixed small whitespace issues.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 49
diff changeset
   832
    Drule.instantiate' [SOME cT, SOME cT, SOME @{ctyp bool}] [NONE, NONE, NONE, NONE, SOME (@{cpat "op ="})] @{thm arg_cong2}
19
55aefc2d524a The tactic still only for fset
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 18
diff changeset
   833
  )
55aefc2d524a The tactic still only for fset
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 18
diff changeset
   834
*}
55aefc2d524a The tactic still only for fset
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 18
diff changeset
   835
18
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   836
ML {*
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   837
  fun split_binop_conv t =
18
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   838
    let
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   839
      val (lhs, rhs) = dest_ceq t;
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   840
      val (bop, _) = dest_cbinop lhs;
19
55aefc2d524a The tactic still only for fset
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 18
diff changeset
   841
      val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
55aefc2d524a The tactic still only for fset
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 18
diff changeset
   842
      val [cmT, crT] = Thm.dest_ctyp cr2;
18
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   843
    in
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   844
      Drule.instantiate' [SOME clT, SOME cmT, SOME crT] [NONE, NONE, NONE, NONE, SOME bop] @{thm arg_cong2}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   845
    end
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   846
*}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   847
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   848
ML {*
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   849
  fun split_arg_conv t =
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   850
    let
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   851
      val (lhs, rhs) = dest_ceq t;
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   852
      val (lop, larg) = Thm.dest_comb lhs;
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   853
      val [caT, crT] = lop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   854
    in
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   855
      Drule.instantiate' [SOME caT, SOME crT] [NONE, NONE, SOME lop] @{thm arg_cong}
35
fdc5962936fa Correctly handling abstractions while building goals
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 34
diff changeset
   856
    end
fdc5962936fa Correctly handling abstractions while building goals
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 34
diff changeset
   857
*}
fdc5962936fa Correctly handling abstractions while building goals
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 34
diff changeset
   858
fdc5962936fa Correctly handling abstractions while building goals
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 34
diff changeset
   859
ML {*
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   860
  fun split_binop_tac n thm =
18
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   861
    let
19
55aefc2d524a The tactic still only for fset
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 18
diff changeset
   862
      val concl = Thm.cprem_of thm n;
55aefc2d524a The tactic still only for fset
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 18
diff changeset
   863
      val (_, cconcl) = Thm.dest_comb concl;
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   864
      val rewr = split_binop_conv cconcl;
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   865
    in
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   866
      rtac rewr n thm
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   867
    end
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   868
      handle CTERM _ => Seq.empty
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   869
*}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   870
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   871
ML {*
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   872
  fun split_arg_tac n thm =
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   873
    let
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   874
      val concl = Thm.cprem_of thm n;
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   875
      val (_, cconcl) = Thm.dest_comb concl;
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   876
      val rewr = split_arg_conv cconcl;
18
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   877
    in
19
55aefc2d524a The tactic still only for fset
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 18
diff changeset
   878
      rtac rewr n thm
18
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   879
    end
19
55aefc2d524a The tactic still only for fset
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 18
diff changeset
   880
      handle CTERM _ => Seq.empty
18
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   881
*}
19
55aefc2d524a The tactic still only for fset
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 18
diff changeset
   882
20
ccc220a23887 Testing the tactic further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 19
diff changeset
   883
(* Has all the theorems about fset plugged in. These should be parameters to the tactic *)
ccc220a23887 Testing the tactic further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 19
diff changeset
   884
32
999300935e9c Make the tactic use Trueprop_cong and atomize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 31
diff changeset
   885
lemma trueprop_cong:
999300935e9c Make the tactic use Trueprop_cong and atomize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 31
diff changeset
   886
  shows "(a \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)"
999300935e9c Make the tactic use Trueprop_cong and atomize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 31
diff changeset
   887
  by auto
999300935e9c Make the tactic use Trueprop_cong and atomize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 31
diff changeset
   888
57
13be92f5b638 used new cong_tac
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   889
ML {*
13be92f5b638 used new cong_tac
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   890
  Cong_Tac.cong_tac
13be92f5b638 used new cong_tac
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   891
*}
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   892
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   893
thm QUOT_TYPE_I_fset.R_trans2
19
55aefc2d524a The tactic still only for fset
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 18
diff changeset
   894
ML {*
25
9020ee23a020 The tactic with REPEAT, CHANGED and a proper simpset.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 24
diff changeset
   895
  fun foo_tac' ctxt =
9020ee23a020 The tactic with REPEAT, CHANGED and a proper simpset.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 24
diff changeset
   896
    REPEAT_ALL_NEW (FIRST' [
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   897
(*      rtac @{thm trueprop_cong},*)
47
6a51704204e5 consistent state
Christian Urban <urbanc@in.tum.de>
parents: 46
diff changeset
   898
      rtac @{thm list_eq_refl},
19
55aefc2d524a The tactic still only for fset
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 18
diff changeset
   899
      rtac @{thm cons_preserves},
55aefc2d524a The tactic still only for fset
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 18
diff changeset
   900
      rtac @{thm mem_respects},
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   901
      rtac @{thm card1_rsp},
25
9020ee23a020 The tactic with REPEAT, CHANGED and a proper simpset.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 24
diff changeset
   902
      rtac @{thm QUOT_TYPE_I_fset.R_trans2},
9020ee23a020 The tactic with REPEAT, CHANGED and a proper simpset.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 24
diff changeset
   903
      CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})),
57
13be92f5b638 used new cong_tac
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   904
      Cong_Tac.cong_tac @{thm cong},
58
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
   905
      rtac @{thm ext}
51
32c0985563a8 Tested new build_goal and removed old one, eq_reflection is included in atomize, card_suc tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 50
diff changeset
   906
(*      rtac @{thm eq_reflection},*)
58
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
   907
(*      CHANGED o (ObjectLogic.full_atomize_tac)*)
25
9020ee23a020 The tactic with REPEAT, CHANGED and a proper simpset.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 24
diff changeset
   908
    ])
19
55aefc2d524a The tactic still only for fset
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 18
diff changeset
   909
*}
55aefc2d524a The tactic still only for fset
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 18
diff changeset
   910
20
ccc220a23887 Testing the tactic further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 19
diff changeset
   911
ML {*
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   912
  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))
55
b2ab3ba388a0 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 54
diff changeset
   913
  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
20
ccc220a23887 Testing the tactic further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 19
diff changeset
   914
  val cgoal = cterm_of @{theory} goal
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   915
  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
20
ccc220a23887 Testing the tactic further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 19
diff changeset
   916
*}
ccc220a23887 Testing the tactic further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 19
diff changeset
   917
30
e35198635d64 Using "atomize" the versions with arbitrary Trueprops can be proven.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 29
diff changeset
   918
(*notation ( output) "prop" ("#_" [1000] 1000) *)
e35198635d64 Using "atomize" the versions with arbitrary Trueprops can be proven.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 29
diff changeset
   919
notation ( output) "Trueprop" ("#_" [1000] 1000)
29
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
   920
70
f3cbda066c3a consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   921
lemma atomize_eqv[atomize]: 
f3cbda066c3a consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   922
  shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" 
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   923
proof
70
f3cbda066c3a consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   924
  assume "A \<equiv> B" 
f3cbda066c3a consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   925
  then show "Trueprop A \<equiv> Trueprop B" by unfold
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   926
next
70
f3cbda066c3a consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   927
  assume *: "Trueprop A \<equiv> Trueprop B"
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   928
  have "A = B"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   929
  proof (cases A)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   930
    case True
70
f3cbda066c3a consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   931
    have "A" by fact
f3cbda066c3a consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   932
    then show "A = B" using * by simp
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   933
  next
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   934
    case False
70
f3cbda066c3a consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   935
    have "\<not>A" by fact
f3cbda066c3a consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   936
    then show "A = B" using * by auto
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   937
  qed
70
f3cbda066c3a consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   938
  then show "A \<equiv> B" by (rule eq_reflection)
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   939
qed
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   940
30
e35198635d64 Using "atomize" the versions with arbitrary Trueprops can be proven.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 29
diff changeset
   941
prove {* (Thm.term_of cgoal2) *}
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   942
  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
58
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
   943
  apply (atomize(full))
25
9020ee23a020 The tactic with REPEAT, CHANGED and a proper simpset.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 24
diff changeset
   944
  apply (tactic {* foo_tac' @{context} 1 *})
30
e35198635d64 Using "atomize" the versions with arbitrary Trueprops can be proven.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 29
diff changeset
   945
  done
18
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
   946
20
ccc220a23887 Testing the tactic further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 19
diff changeset
   947
thm length_append (* Not true but worth checking that the goal is correct *)
ccc220a23887 Testing the tactic further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 19
diff changeset
   948
ML {*
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   949
  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm length_append}))
55
b2ab3ba388a0 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 54
diff changeset
   950
  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
20
ccc220a23887 Testing the tactic further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 19
diff changeset
   951
  val cgoal = cterm_of @{theory} goal
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   952
  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
20
ccc220a23887 Testing the tactic further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 19
diff changeset
   953
*}
30
e35198635d64 Using "atomize" the versions with arbitrary Trueprops can be proven.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 29
diff changeset
   954
prove {* Thm.term_of cgoal2 *}
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   955
  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
58
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
   956
  apply (atomize(full))
30
e35198635d64 Using "atomize" the versions with arbitrary Trueprops can be proven.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 29
diff changeset
   957
  apply (tactic {* foo_tac' @{context} 1 *})
25
9020ee23a020 The tactic with REPEAT, CHANGED and a proper simpset.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 24
diff changeset
   958
  sorry
19
55aefc2d524a The tactic still only for fset
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 18
diff changeset
   959
20
ccc220a23887 Testing the tactic further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 19
diff changeset
   960
thm m2
ccc220a23887 Testing the tactic further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 19
diff changeset
   961
ML {*
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   962
  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
55
b2ab3ba388a0 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 54
diff changeset
   963
  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
20
ccc220a23887 Testing the tactic further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 19
diff changeset
   964
  val cgoal = cterm_of @{theory} goal
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   965
  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
20
ccc220a23887 Testing the tactic further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 19
diff changeset
   966
*}
30
e35198635d64 Using "atomize" the versions with arbitrary Trueprops can be proven.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 29
diff changeset
   967
prove {* Thm.term_of cgoal2 *}
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   968
  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
58
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
   969
  apply (atomize(full))
30
e35198635d64 Using "atomize" the versions with arbitrary Trueprops can be proven.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 29
diff changeset
   970
  apply (tactic {* foo_tac' @{context} 1 *})
e35198635d64 Using "atomize" the versions with arbitrary Trueprops can be proven.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 29
diff changeset
   971
  done
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   972
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   973
thm list_eq.intros(4)
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   974
ML {*
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   975
  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)}))
55
b2ab3ba388a0 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 54
diff changeset
   976
  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   977
  val cgoal = cterm_of @{theory} goal
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   978
  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
24
6885fa184e89 Merged with my changes from the morning:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 23
diff changeset
   979
  val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2)
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   980
*}
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   981
24
6885fa184e89 Merged with my changes from the morning:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 23
diff changeset
   982
(* It is the same, but we need a name for it. *)
52
6584b1ceedce Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 51
diff changeset
   983
prove zzz : {* Thm.term_of cgoal3 *}
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   984
  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
58
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
   985
  apply (atomize(full))
25
9020ee23a020 The tactic with REPEAT, CHANGED and a proper simpset.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 24
diff changeset
   986
  apply (tactic {* foo_tac' @{context} 1 *})
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   987
  done
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   988
24
6885fa184e89 Merged with my changes from the morning:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 23
diff changeset
   989
lemma zzz' :
6885fa184e89 Merged with my changes from the morning:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 23
diff changeset
   990
  "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))"
6885fa184e89 Merged with my changes from the morning:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 23
diff changeset
   991
  using list_eq.intros(4) by (simp only: zzz)
6885fa184e89 Merged with my changes from the morning:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 23
diff changeset
   992
6885fa184e89 Merged with my changes from the morning:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 23
diff changeset
   993
thm QUOT_TYPE_I_fset.REPS_same
25
9020ee23a020 The tactic with REPEAT, CHANGED and a proper simpset.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 24
diff changeset
   994
ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *}
9020ee23a020 The tactic with REPEAT, CHANGED and a proper simpset.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 24
diff changeset
   995
46
e801b929216b some tuning of my code
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   996
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   997
thm list_eq.intros(5)
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
   998
ML {*
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
   999
  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)}))
55
b2ab3ba388a0 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 54
diff changeset
  1000
  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
38
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
  1001
*}
cac00e8b972b tuned slightly one proof
Christian Urban <urbanc@in.tum.de>
parents: 37
diff changeset
  1002
ML {*
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1003
  val cgoal =
29
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
  1004
    Toplevel.program (fn () =>
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
  1005
      cterm_of @{theory} goal
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
  1006
    )
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
  1007
*}
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
  1008
ML {*
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1009
  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
  1010
*}
30
e35198635d64 Using "atomize" the versions with arbitrary Trueprops can be proven.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 29
diff changeset
  1011
prove {* Thm.term_of cgoal2 *}
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
  1012
  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
58
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
  1013
  apply (atomize(full))
25
9020ee23a020 The tactic with REPEAT, CHANGED and a proper simpset.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 24
diff changeset
  1014
  apply (tactic {* foo_tac' @{context} 1 *})
21
d15121412caa Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 20
diff changeset
  1015
  done
18
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
  1016
29
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
  1017
thm list.induct
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
  1018
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
  1019
ML {*
50
18d8bcd769b3 Checked again with the version on my hard-drive backedup yesterday and fixed small whitespace issues.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 49
diff changeset
  1020
  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct}))
29
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
  1021
*}
58
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
  1022
29
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
  1023
ML {*
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
  1024
  val goal =
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
  1025
    Toplevel.program (fn () =>
55
b2ab3ba388a0 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 54
diff changeset
  1026
      build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
29
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
  1027
    )
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
  1028
*}
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
  1029
ML {*
55
b2ab3ba388a0 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 54
diff changeset
  1030
  val cgoal = 
b2ab3ba388a0 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 54
diff changeset
  1031
    Toplevel.program (fn () =>
b2ab3ba388a0 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 54
diff changeset
  1032
      cterm_of @{theory} goal
b2ab3ba388a0 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 54
diff changeset
  1033
    )
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1034
  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
35
fdc5962936fa Correctly handling abstractions while building goals
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 34
diff changeset
  1035
*}
50
18d8bcd769b3 Checked again with the version on my hard-drive backedup yesterday and fixed small whitespace issues.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 49
diff changeset
  1036
33
e8f1fa50329a Found the source for the exception and added a handle for it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 32
diff changeset
  1037
prove {* (Thm.term_of cgoal2) *}
e8f1fa50329a Found the source for the exception and added a handle for it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 32
diff changeset
  1038
  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
58
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
  1039
  apply (atomize(full))
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1040
  apply (tactic {* foo_tac' @{context} 1 *})
33
e8f1fa50329a Found the source for the exception and added a handle for it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 32
diff changeset
  1041
  sorry
29
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
  1042
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1043
ML {*
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1044
  fun lift_theorem_fset_aux thm lthy =
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1045
    let
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1046
      val ((_, [novars]), lthy2) = Variable.import true [thm] lthy;
55
b2ab3ba388a0 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 54
diff changeset
  1047
      val goal = build_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs;
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1048
      val cgoal = cterm_of @{theory} goal;
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1049
      val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal);
58
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
  1050
      val tac = (LocalDefs.unfold_tac @{context} fset_defs) THEN (ObjectLogic.full_atomize_tac 1) THEN (foo_tac' @{context}) 1;
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1051
      val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac);
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1052
      val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm)))
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1053
      val nthm2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same QUOT_TYPE_I_fset.thm10} nthm;
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1054
      val [nthm3] = ProofContext.export lthy2 lthy [nthm2]
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1055
    in
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1056
      nthm3
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1057
    end
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1058
*}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1059
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1060
ML {* lift_theorem_fset_aux @{thm m1} @{context} *}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1061
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1062
ML {*
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1063
  fun lift_theorem_fset name thm lthy =
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1064
    let
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1065
      val lifted_thm = lift_theorem_fset_aux thm lthy;
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1066
      val (_, lthy2) = note_thm (name, lifted_thm) lthy;
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1067
    in
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1068
      lthy2
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1069
    end;
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1070
*}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1071
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1072
local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1073
local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1074
local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1075
local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *}
58
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
  1076
(*ML {* Toplevel.program (fn () => lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} @{context}) *}
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
  1077
local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*)
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1078
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1079
thm m1_lift
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1080
thm leqi4_lift
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1081
thm leqi5_lift
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1082
thm m2_lift
56
ec5fbe7ab427 First version of handling of the universal quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 55
diff changeset
  1083
(*thm card_suc*)
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1084
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1085
thm leqi4_lift
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1086
ML {*
62
58384c90a5e5 used prop_of to get the term of a theorem (replaces crep_thm)
Christian Urban <urbanc@in.tum.de>
parents: 61
diff changeset
  1087
  val (nam, typ) = hd (Term.add_vars (prop_of @{thm leqi4_lift}) [])
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1088
  val (_, l) = dest_Type typ
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1089
  val t = Type ("QuotMain.fset", l)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1090
  val v = Var (nam, t)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1091
  val cv = cterm_of @{theory} ((term_of @{cpat "REP_fset"}) $ v)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1092
*}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1093
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1094
ML {*
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1095
  Toplevel.program (fn () =>
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1096
    MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} (
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1097
      Drule.instantiate' [] [NONE, SOME (cv)] @{thm leqi4_lift}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1098
    )
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1099
  )
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1100
*}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1101
56
ec5fbe7ab427 First version of handling of the universal quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 55
diff changeset
  1102
(*
52
6584b1ceedce Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 51
diff changeset
  1103
thm card_suc
6584b1ceedce Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 51
diff changeset
  1104
ML {*
62
58384c90a5e5 used prop_of to get the term of a theorem (replaces crep_thm)
Christian Urban <urbanc@in.tum.de>
parents: 61
diff changeset
  1105
  val (nam, typ) = hd (tl (Term.add_vars (prop_of @{thm card_suc})) [])
52
6584b1ceedce Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 51
diff changeset
  1106
  val (_, l) = dest_Type typ
6584b1ceedce Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 51
diff changeset
  1107
  val t = Type ("QuotMain.fset", l)
6584b1ceedce Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 51
diff changeset
  1108
  val v = Var (nam, t)
6584b1ceedce Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 51
diff changeset
  1109
  val cv = cterm_of @{theory} ((term_of @{cpat "REP_fset"}) $ v)
6584b1ceedce Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 51
diff changeset
  1110
*}
6584b1ceedce Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 51
diff changeset
  1111
6584b1ceedce Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 51
diff changeset
  1112
ML {*
6584b1ceedce Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 51
diff changeset
  1113
  Toplevel.program (fn () =>
6584b1ceedce Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 51
diff changeset
  1114
    MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} (
6584b1ceedce Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 51
diff changeset
  1115
      Drule.instantiate' [] [SOME (cv)] @{thm card_suc}
6584b1ceedce Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 51
diff changeset
  1116
    )
6584b1ceedce Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 51
diff changeset
  1117
  )
6584b1ceedce Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 51
diff changeset
  1118
*}
56
ec5fbe7ab427 First version of handling of the universal quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 55
diff changeset
  1119
*)
52
6584b1ceedce Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 51
diff changeset
  1120
6584b1ceedce Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 51
diff changeset
  1121
6584b1ceedce Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 51
diff changeset
  1122
6584b1ceedce Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 51
diff changeset
  1123
29
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
  1124
thm card1_suc
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
  1125
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
  1126
ML {*
50
18d8bcd769b3 Checked again with the version on my hard-drive backedup yesterday and fixed small whitespace issues.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 49
diff changeset
  1127
  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm card1_suc}))
29
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
  1128
*}
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
  1129
ML {*
55
b2ab3ba388a0 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 54
diff changeset
  1130
  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
29
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
  1131
*}
56
ec5fbe7ab427 First version of handling of the universal quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 55
diff changeset
  1132
ML {* term_of @{cpat "all"} *}
29
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
  1133
ML {*
56
ec5fbe7ab427 First version of handling of the universal quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 55
diff changeset
  1134
  val cgoal = 
ec5fbe7ab427 First version of handling of the universal quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 55
diff changeset
  1135
    Toplevel.program (fn () =>
ec5fbe7ab427 First version of handling of the universal quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 55
diff changeset
  1136
      cterm_of @{theory} goal
ec5fbe7ab427 First version of handling of the universal quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 55
diff changeset
  1137
    );
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1138
  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
29
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
  1139
*}
73
fdaf1466daf0 Further experiments with proving induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 72
diff changeset
  1140
fdaf1466daf0 Further experiments with proving induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 72
diff changeset
  1141
definition
77
cb74afa437d7 Bounded quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 76
diff changeset
  1142
  "x IN p ==> (Babs p m x = m x)"
72
4efc9e6661a4 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 71
diff changeset
  1143
74
0370493040f3 Further with the manual proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 73
diff changeset
  1144
print_theorems
77
cb74afa437d7 Bounded quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 76
diff changeset
  1145
thm Babs_def
74
0370493040f3 Further with the manual proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 73
diff changeset
  1146
77
cb74afa437d7 Bounded quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 76
diff changeset
  1147
lemma "(Ball (Respects ((op \<approx>) ===> (op =)))
72
4efc9e6661a4 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 71
diff changeset
  1148
         (((REP_fset ---> id) ---> id)
4efc9e6661a4 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 71
diff changeset
  1149
             (((ABS_fset ---> id) ---> id)
4efc9e6661a4 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 71
diff changeset
  1150
               (\<lambda>P.
4efc9e6661a4 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 71
diff changeset
  1151
                  (ABS_fset ---> id) ((REP_fset ---> id) P)
4efc9e6661a4 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 71
diff changeset
  1152
                    (REP_fset (ABS_fset [])) \<and>
77
cb74afa437d7 Bounded quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 76
diff changeset
  1153
                  Ball (Respects (op \<approx>))
72
4efc9e6661a4 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 71
diff changeset
  1154
                    ((ABS_fset ---> id)
4efc9e6661a4 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 71
diff changeset
  1155
                       ((REP_fset ---> id)
4efc9e6661a4 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 71
diff changeset
  1156
                          (\<lambda>t.
4efc9e6661a4 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 71
diff changeset
  1157
                             ((ABS_fset ---> id)
4efc9e6661a4 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 71
diff changeset
  1158
                               ((REP_fset ---> id) P)
73
fdaf1466daf0 Further experiments with proving induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 72
diff changeset
  1159
                               (REP_fset (ABS_fset t))) \<longrightarrow>
72
4efc9e6661a4 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 71
diff changeset
  1160
                             (!h.
4efc9e6661a4 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 71
diff changeset
  1161
                               (ABS_fset ---> id)
4efc9e6661a4 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 71
diff changeset
  1162
                                 ((REP_fset ---> id) P)
4efc9e6661a4 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 71
diff changeset
  1163
                                 (REP_fset
4efc9e6661a4 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 71
diff changeset
  1164
                                    (ABS_fset
4efc9e6661a4 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 71
diff changeset
  1165
                                       (h #
4efc9e6661a4 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 71
diff changeset
  1166
                                            REP_fset
73
fdaf1466daf0 Further experiments with proving induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 72
diff changeset
  1167
                                              (ABS_fset t)))))))) \<longrightarrow>
77
cb74afa437d7 Bounded quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 76
diff changeset
  1168
                  Ball (Respects (op \<approx>))
72
4efc9e6661a4 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 71
diff changeset
  1169
                    ((ABS_fset ---> id)
4efc9e6661a4 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 71
diff changeset
  1170
                       ((REP_fset ---> id)
4efc9e6661a4 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 71
diff changeset
  1171
                          (\<lambda>l.
4efc9e6661a4 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 71
diff changeset
  1172
                             (ABS_fset ---> id)
4efc9e6661a4 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 71
diff changeset
  1173
                               ((REP_fset ---> id) P)
74
0370493040f3 Further with the manual proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 73
diff changeset
  1174
                               (REP_fset (ABS_fset l)))))))))
0370493040f3 Further with the manual proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 73
diff changeset
  1175
77
cb74afa437d7 Bounded quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 76
diff changeset
  1176
   = Ball (Respects ((op \<approx>) ===> (op =)))
cb74afa437d7 Bounded quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 76
diff changeset
  1177
     (\<lambda>P. ((P []) \<and> (Ball (Respects (op \<approx>)) (\<lambda>t. P t \<longrightarrow> (\<forall>h. (P (h # t)))))) \<longrightarrow>
cb74afa437d7 Bounded quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 76
diff changeset
  1178
     (Ball (Respects (op \<approx>)) (\<lambda>l. P l)))"
74
0370493040f3 Further with the manual proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 73
diff changeset
  1179
term "(\<forall>P. (((P []) \<and> (\<forall>t. (P t \<longrightarrow> (\<forall>h. P (h # t))))) \<longrightarrow> (\<forall>l. (P l))))"
73
fdaf1466daf0 Further experiments with proving induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 72
diff changeset
  1180
thm LAMBDA_PRS1[symmetric]
fdaf1466daf0 Further experiments with proving induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 72
diff changeset
  1181
(*apply (simp only:LAMBDA_PRS1[symmetric] FUN_QUOTIENT IDENTITY_QUOTIENT QUOT_TYPE_I_fset.QUOTIENT)*)
77
cb74afa437d7 Bounded quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 76
diff changeset
  1182
apply (unfold Ball_def)
74
0370493040f3 Further with the manual proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 73
diff changeset
  1183
apply (simp only: IN_RESPECTS)
0370493040f3 Further with the manual proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 73
diff changeset
  1184
apply (simp only:list_eq_refl)
72
4efc9e6661a4 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 71
diff changeset
  1185
apply (unfold id_def)
74
0370493040f3 Further with the manual proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 73
diff changeset
  1186
(*apply (simp only: FUN_MAP_I)*)
0370493040f3 Further with the manual proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 73
diff changeset
  1187
apply (simp)
0370493040f3 Further with the manual proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 73
diff changeset
  1188
apply (simp only: QUOT_TYPE_I_fset.thm10)
0370493040f3 Further with the manual proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 73
diff changeset
  1189
apply (tactic {* foo_tac' @{context} 1 *})
0370493040f3 Further with the manual proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 73
diff changeset
  1190
0370493040f3 Further with the manual proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 73
diff changeset
  1191
..
73
fdaf1466daf0 Further experiments with proving induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 72
diff changeset
  1192
apply (simp add:IN_RESPECTS)
74
0370493040f3 Further with the manual proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 73
diff changeset
  1193
73
fdaf1466daf0 Further experiments with proving induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 72
diff changeset
  1194
fdaf1466daf0 Further experiments with proving induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 72
diff changeset
  1195
fdaf1466daf0 Further experiments with proving induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 72
diff changeset
  1196
fdaf1466daf0 Further experiments with proving induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 72
diff changeset
  1197
apply (simp add: QUOT_TYPE_I_fset.R_trans2)
fdaf1466daf0 Further experiments with proving induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 72
diff changeset
  1198
fdaf1466daf0 Further experiments with proving induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 72
diff changeset
  1199
apply (rule ext)
fdaf1466daf0 Further experiments with proving induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 72
diff changeset
  1200
apply (simp add:QUOT_TYPE_I_fset.REP_ABS_rsp)
fdaf1466daf0 Further experiments with proving induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 72
diff changeset
  1201
apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *} )
fdaf1466daf0 Further experiments with proving induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 72
diff changeset
  1202
apply (simp add:cons_preserves)
fdaf1466daf0 Further experiments with proving induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 72
diff changeset
  1203
fdaf1466daf0 Further experiments with proving induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 72
diff changeset
  1204
72
4efc9e6661a4 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 71
diff changeset
  1205
4efc9e6661a4 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 71
diff changeset
  1206
(*prove aaa: {* (Thm.term_of cgoal2) *}
45
d98224cafb86 Cleanup
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 44
diff changeset
  1207
  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
58
f2565006dc5a Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 57
diff changeset
  1208
  apply (atomize(full))
49
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 47
diff changeset
  1209
  apply (tactic {* foo_tac' @{context} 1 *})
72
4efc9e6661a4 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 71
diff changeset
  1210
  done*)
29
2b59bf690633 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 28
diff changeset
  1211
18
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
  1212
(*
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
  1213
datatype obj1 =
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
  1214
  OVAR1 "string"
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
  1215
| OBJ1 "(string * (string \<Rightarrow> obj1)) list"
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
  1216
| INVOKE1 "obj1 \<Rightarrow> string"
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
  1217
| UPDATE1 "obj1 \<Rightarrow> string \<Rightarrow> (string \<Rightarrow> obj1)"
ce522150c1f7 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 17
diff changeset
  1218
*)
53
a036f6fb1516 Test line
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 52
diff changeset
  1219
57
13be92f5b638 used new cong_tac
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
  1220
end