(*notation ( output) "prop" ("#_" [1000] 1000) *)+ −
notation ( output) "Trueprop" ("#_" [1000] 1000)+ −
+ −
function(sequential)+ −
akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)+ −
and aty :: "ty \<Rightarrow> ty \<Rightarrow> bool" ("_ \<approx>ty _" [100, 100] 100)+ −
and atrm :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<approx>tr _" [100, 100] 100)+ −
where+ −
a1: "(Type) \<approx>ki (Type) = True"+ −
| 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')))"+ −
| "_ \<approx>ki _ = False"+ −
| a3: "(TConst i) \<approx>ty (TConst j) = (i = j)"+ −
| a4: "(TApp A M) \<approx>ty (TApp A' M') = (A \<approx>ty A' \<and> M \<approx>tr M')"+ −
| 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'))"+ −
| "_ \<approx>ty _ = False"+ −
| a6: "(Const i) \<approx>tr (Const j) = (i = j)"+ −
| a7: "(Var x) \<approx>tr (Var y) = (x = y)"+ −
| a8: "(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')"+ −
| 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'))"+ −
| "_ \<approx>tr _ = False"+ −
apply (pat_completeness)+ −
apply simp_all+ −
done+ −
termination+ −
by (size_change)+ −
+ −
+ −
+ −
lemma regularize_to_injection:+ −
shows "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y"+ −
by(auto simp add: QUOT_TRUE_def)+ −
+ −
syntax+ −
"Bex1_rel" :: "id \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" ("(3\<exists>!!_\<in>_./ _)" [0, 0, 10] 10)+ −
translations+ −
"\<exists>!!x\<in>A. P" == "Bex1_rel A (%x. P)"+ −
+ −
+ −
(* Atomize infrastructure *)+ −
(* FIXME/TODO: is this really needed? *)+ −
(*+ −
lemma atomize_eqv:+ −
shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"+ −
proof+ −
assume "A \<equiv> B"+ −
then show "Trueprop A \<equiv> Trueprop B" by unfold+ −
next+ −
assume *: "Trueprop A \<equiv> Trueprop B"+ −
have "A = B"+ −
proof (cases A)+ −
case True+ −
have "A" by fact+ −
then show "A = B" using * by simp+ −
next+ −
case False+ −
have "\<not>A" by fact+ −
then show "A = B" using * by auto+ −
qed+ −
then show "A \<equiv> B" by (rule eq_reflection)+ −
qed+ −
*)+ −
+ −
+ −
ML {*+ −
fun dest_cbinop t =+ −
let+ −
val (t2, rhs) = Thm.dest_comb t;+ −
val (bop, lhs) = Thm.dest_comb t2;+ −
in+ −
(bop, (lhs, rhs))+ −
end+ −
*}+ −
+ −
ML {*+ −
fun dest_ceq t =+ −
let+ −
val (bop, pair) = dest_cbinop t;+ −
val (bop_s, _) = Term.dest_Const (Thm.term_of bop);+ −
in+ −
if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t]))+ −
end+ −
*}+ −
+ −
ML {*+ −
fun split_binop_conv t =+ −
let+ −
val (lhs, rhs) = dest_ceq t;+ −
val (bop, _) = dest_cbinop lhs;+ −
val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp;+ −
val [cmT, crT] = Thm.dest_ctyp cr2;+ −
in+ −
Drule.instantiate' [SOME clT, SOME cmT, SOME crT] [NONE, NONE, NONE, NONE, SOME bop] @{thm arg_cong2}+ −
end+ −
*}+ −
+ −
+ −
ML {*+ −
fun split_arg_conv t =+ −
let+ −
val (lhs, rhs) = dest_ceq t;+ −
val (lop, larg) = Thm.dest_comb lhs;+ −
val [caT, crT] = lop |> Thm.ctyp_of_term |> Thm.dest_ctyp;+ −
in+ −
Drule.instantiate' [SOME caT, SOME crT] [NONE, NONE, SOME lop] @{thm arg_cong}+ −
end+ −
*}+ −
+ −
ML {*+ −
fun split_binop_tac n thm =+ −
let+ −
val concl = Thm.cprem_of thm n;+ −
val (_, cconcl) = Thm.dest_comb concl;+ −
val rewr = split_binop_conv cconcl;+ −
in+ −
rtac rewr n thm+ −
end+ −
handle CTERM _ => Seq.empty+ −
*}+ −
+ −
+ −
ML {*+ −
fun split_arg_tac n thm =+ −
let+ −
val concl = Thm.cprem_of thm n;+ −
val (_, cconcl) = Thm.dest_comb concl;+ −
val rewr = split_arg_conv cconcl;+ −
in+ −
rtac rewr n thm+ −
end+ −
handle CTERM _ => Seq.empty+ −
*}+ −
+ −
+ −
lemma trueprop_cong:+ −
shows "(a \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)"+ −
by auto+ −
+ −
lemma list_induct_hol4:+ −
fixes P :: "'a list \<Rightarrow> bool"+ −
assumes a: "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))"+ −
shows "\<forall>l. (P l)"+ −
using a+ −
apply (rule_tac allI)+ −
apply (induct_tac "l")+ −
apply (simp)+ −
apply (metis)+ −
done+ −
+ −
ML {*+ −
val no_vars = Thm.rule_attribute (fn context => fn th =>+ −
let+ −
val ctxt = Variable.set_body false (Context.proof_of context);+ −
val ((_, [th']), _) = Variable.import true [th] ctxt;+ −
in th' end);+ −
*}+ −
+ −
(*lemma equality_twice:+ −
"a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)"+ −
by auto*)+ −
+ −
+ −
(*interpretation code *)+ −
(*val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))+ −
val ((_, [eqn1pre]), lthy5) = Variable.import true [ABS_def] lthy4;+ −
val eqn1i = Thm.prop_of (symmetric eqn1pre)+ −
val ((_, [eqn2pre]), lthy6) = Variable.import true [REP_def] lthy5;+ −
val eqn2i = Thm.prop_of (symmetric eqn2pre)+ −
+ −
val exp_morphism = ProofContext.export_morphism lthy6 (ProofContext.init (ProofContext.theory_of lthy6));+ −
val exp_term = Morphism.term exp_morphism;+ −
val exp = Morphism.thm exp_morphism;+ −
+ −
val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN+ −
ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))])))+ −
val mthdt = Method.Basic (fn _ => mthd)+ −
val bymt = Proof.global_terminal_proof (mthdt, NONE)+ −
val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true),+ −
Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))]*)+ −
+ −
(*||> Local_Theory.theory (fn thy =>+ −
let+ −
val global_eqns = map exp_term [eqn2i, eqn1i];+ −
(* Not sure if the following context should not be used *)+ −
val (global_eqns2, lthy7) = Variable.import_terms true global_eqns lthy6;+ −
val global_eqns3 = map (fn t => (bindd, t)) global_eqns2;+ −
in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)*)+ −