226
+ − 1
(*notation ( output) "prop" ("#_" [1000] 1000) *)
+ − 2
notation ( output) "Trueprop" ("#_" [1000] 1000)
101
+ − 3
1024
+ − 4
function(sequential)
+ − 5
akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
+ − 6
and aty :: "ty \<Rightarrow> ty \<Rightarrow> bool" ("_ \<approx>ty _" [100, 100] 100)
+ − 7
and atrm :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<approx>tr _" [100, 100] 100)
+ − 8
where
+ − 9
a1: "(Type) \<approx>ki (Type) = True"
+ − 10
| a2: "(KPi A x K) \<approx>ki (KPi A' x' K') = (A \<approx>ty A' \<and> (\<exists>pi. (rfv_kind K - {atom x} = rfv_kind K' - {atom x'} \<and> (rfv_kind K - {atom x})\<sharp>* pi \<and> (pi \<bullet> K) \<approx>ki K' \<and> (pi \<bullet> x) = x')))"
+ − 11
| "_ \<approx>ki _ = False"
+ − 12
| a3: "(TConst i) \<approx>ty (TConst j) = (i = j)"
+ − 13
| a4: "(TApp A M) \<approx>ty (TApp A' M') = (A \<approx>ty A' \<and> M \<approx>tr M')"
+ − 14
| a5: "(TPi A x B) \<approx>ty (TPi A' x' B') = ((A \<approx>ty A') \<and> (\<exists>pi. rfv_ty B - {atom x} = rfv_ty B' - {atom x'} \<and> (rfv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) \<approx>ty B' \<and> (pi \<bullet> x) = x'))"
+ − 15
| "_ \<approx>ty _ = False"
+ − 16
| a6: "(Const i) \<approx>tr (Const j) = (i = j)"
+ − 17
| a7: "(Var x) \<approx>tr (Var y) = (x = y)"
+ − 18
| a8: "(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')"
+ − 19
| a9: "(Lam A x M) \<approx>tr (Lam A' x' M') = (A \<approx>ty A' \<and> (\<exists>pi. rfv_trm M - {atom x} = rfv_trm M' - {atom x'} \<and> (rfv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) \<approx>tr M' \<and> (pi \<bullet> x) = x'))"
+ − 20
| "_ \<approx>tr _ = False"
+ − 21
apply (pat_completeness)
+ − 22
apply simp_all
+ − 23
done
+ − 24
termination
+ − 25
by (size_change)
+ − 26
+ − 27
+ − 28
806
43336511993f
Readded 'regularize_to_injection' which I believe will be needed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 29
lemma regularize_to_injection:
43336511993f
Readded 'regularize_to_injection' which I believe will be needed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 30
shows "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y"
43336511993f
Readded 'regularize_to_injection' which I believe will be needed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 31
by(auto simp add: QUOT_TRUE_def)
43336511993f
Readded 'regularize_to_injection' which I believe will be needed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 32
912
+ − 33
syntax
980
+ − 34
"Bex1_rel" :: "id \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" ("(3\<exists>!!_\<in>_./ _)" [0, 0, 10] 10)
912
+ − 35
translations
980
+ − 36
"\<exists>!!x\<in>A. P" == "Bex1_rel A (%x. P)"
806
43336511993f
Readded 'regularize_to_injection' which I believe will be needed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 37
43336511993f
Readded 'regularize_to_injection' which I believe will be needed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 38
870
2a19e0a37131
Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 39
(* Atomize infrastructure *)
2a19e0a37131
Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 40
(* FIXME/TODO: is this really needed? *)
2a19e0a37131
Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 41
(*
2a19e0a37131
Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 42
lemma atomize_eqv:
2a19e0a37131
Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 43
shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
2a19e0a37131
Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 44
proof
2a19e0a37131
Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 45
assume "A \<equiv> B"
2a19e0a37131
Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 46
then show "Trueprop A \<equiv> Trueprop B" by unfold
2a19e0a37131
Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 47
next
2a19e0a37131
Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 48
assume *: "Trueprop A \<equiv> Trueprop B"
2a19e0a37131
Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 49
have "A = B"
2a19e0a37131
Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 50
proof (cases A)
2a19e0a37131
Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 51
case True
2a19e0a37131
Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 52
have "A" by fact
2a19e0a37131
Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 53
then show "A = B" using * by simp
2a19e0a37131
Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 54
next
2a19e0a37131
Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 55
case False
2a19e0a37131
Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 56
have "\<not>A" by fact
2a19e0a37131
Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 57
then show "A = B" using * by auto
2a19e0a37131
Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 58
qed
2a19e0a37131
Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 59
then show "A \<equiv> B" by (rule eq_reflection)
2a19e0a37131
Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 60
qed
2a19e0a37131
Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 61
*)
2a19e0a37131
Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 62
806
43336511993f
Readded 'regularize_to_injection' which I believe will be needed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 63
101
+ − 64
ML {*
+ − 65
fun dest_cbinop t =
+ − 66
let
+ − 67
val (t2, rhs) = Thm.dest_comb t;
+ − 68
val (bop, lhs) = Thm.dest_comb t2;
+ − 69
in
+ − 70
(bop, (lhs, rhs))
+ − 71
end
+ − 72
*}
+ − 73
+ − 74
ML {*
+ − 75
fun dest_ceq t =
+ − 76
let
+ − 77
val (bop, pair) = dest_cbinop t;
+ − 78
val (bop_s, _) = Term.dest_Const (Thm.term_of bop);
+ − 79
in
+ − 80
if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t]))
+ − 81
end
+ − 82
*}
+ − 83
+ − 84
ML {*
+ − 85
fun split_binop_conv t =
+ − 86
let
+ − 87
val (lhs, rhs) = dest_ceq t;
+ − 88
val (bop, _) = dest_cbinop lhs;
+ − 89
val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
+ − 90
val [cmT, crT] = Thm.dest_ctyp cr2;
+ − 91
in
+ − 92
Drule.instantiate' [SOME clT, SOME cmT, SOME crT] [NONE, NONE, NONE, NONE, SOME bop] @{thm arg_cong2}
+ − 93
end
+ − 94
*}
+ − 95
+ − 96
+ − 97
ML {*
+ − 98
fun split_arg_conv t =
+ − 99
let
+ − 100
val (lhs, rhs) = dest_ceq t;
+ − 101
val (lop, larg) = Thm.dest_comb lhs;
+ − 102
val [caT, crT] = lop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
+ − 103
in
+ − 104
Drule.instantiate' [SOME caT, SOME crT] [NONE, NONE, SOME lop] @{thm arg_cong}
+ − 105
end
+ − 106
*}
+ − 107
+ − 108
ML {*
+ − 109
fun split_binop_tac n thm =
+ − 110
let
+ − 111
val concl = Thm.cprem_of thm n;
+ − 112
val (_, cconcl) = Thm.dest_comb concl;
+ − 113
val rewr = split_binop_conv cconcl;
+ − 114
in
+ − 115
rtac rewr n thm
+ − 116
end
+ − 117
handle CTERM _ => Seq.empty
+ − 118
*}
+ − 119
+ − 120
+ − 121
ML {*
+ − 122
fun split_arg_tac n thm =
+ − 123
let
+ − 124
val concl = Thm.cprem_of thm n;
+ − 125
val (_, cconcl) = Thm.dest_comb concl;
+ − 126
val rewr = split_arg_conv cconcl;
+ − 127
in
+ − 128
rtac rewr n thm
+ − 129
end
+ − 130
handle CTERM _ => Seq.empty
+ − 131
*}
+ − 132
+ − 133
+ − 134
lemma trueprop_cong:
303
+ − 135
shows "(a \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)"
101
+ − 136
by auto
226
+ − 137
+ − 138
lemma list_induct_hol4:
303
+ − 139
fixes P :: "'a list \<Rightarrow> bool"
+ − 140
assumes a: "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))"
+ − 141
shows "\<forall>l. (P l)"
226
+ − 142
using a
+ − 143
apply (rule_tac allI)
+ − 144
apply (induct_tac "l")
+ − 145
apply (simp)
+ − 146
apply (metis)
+ − 147
done
+ − 148
301
+ − 149
ML {*
+ − 150
val no_vars = Thm.rule_attribute (fn context => fn th =>
+ − 151
let
+ − 152
val ctxt = Variable.set_body false (Context.proof_of context);
+ − 153
val ((_, [th']), _) = Variable.import true [th] ctxt;
+ − 154
in th' end);
+ − 155
*}
303
+ − 156
+ − 157
(*lemma equality_twice:
+ − 158
"a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)"
+ − 159
by auto*)
685
+ − 160
+ − 161
+ − 162
(*interpretation code *)
+ − 163
(*val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
+ − 164
val ((_, [eqn1pre]), lthy5) = Variable.import true [ABS_def] lthy4;
+ − 165
val eqn1i = Thm.prop_of (symmetric eqn1pre)
+ − 166
val ((_, [eqn2pre]), lthy6) = Variable.import true [REP_def] lthy5;
+ − 167
val eqn2i = Thm.prop_of (symmetric eqn2pre)
+ − 168
+ − 169
val exp_morphism = ProofContext.export_morphism lthy6 (ProofContext.init (ProofContext.theory_of lthy6));
+ − 170
val exp_term = Morphism.term exp_morphism;
+ − 171
val exp = Morphism.thm exp_morphism;
+ − 172
+ − 173
val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN
+ − 174
ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))])))
+ − 175
val mthdt = Method.Basic (fn _ => mthd)
+ − 176
val bymt = Proof.global_terminal_proof (mthdt, NONE)
+ − 177
val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true),
+ − 178
Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))]*)
+ − 179
+ − 180
(*||> Local_Theory.theory (fn thy =>
+ − 181
let
+ − 182
val global_eqns = map exp_term [eqn2i, eqn1i];
+ − 183
(* Not sure if the following context should not be used *)
+ − 184
val (global_eqns2, lthy7) = Variable.import_terms true global_eqns lthy6;
+ − 185
val global_eqns3 = map (fn t => (bindd, t)) global_eqns2;
806
43336511993f
Readded 'regularize_to_injection' which I believe will be needed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 186
in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)*)