(* Title: CCL/hered
ID: $Id$
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
For hered.thy.
*)
open Hered;
fun type_of_terms (Const("Trueprop",_) $ (Const("op =",(Type ("fun", [t,_])))$_$_)) = t;
(*** Hereditary Termination ***)
Goalw [HTTgen_def] "mono(%X. HTTgen(X))";
by (rtac monoI 1);
by (fast_tac set_cs 1);
qed "HTTgen_mono";
Goalw [HTTgen_def]
"t : HTTgen(A) <-> t=true | t=false | (EX a b. t=<a,b> & a : A & b : A) | \
\ (EX f. t=lam x. f(x) & (ALL x. f(x) : A))";
by (fast_tac set_cs 1);
qed "HTTgenXH";
Goal
"t : HTT <-> t=true | t=false | (EX a b. t=<a,b> & a : HTT & b : HTT) | \
\ (EX f. t=lam x. f(x) & (ALL x. f(x) : HTT))";
by (rtac (rewrite_rule [HTTgen_def]
(HTTgen_mono RS (HTT_def RS def_gfp_Tarski) RS XHlemma1)) 1);
by (fast_tac set_cs 1);
qed "HTTXH";
(*** Introduction Rules for HTT ***)
Goal "~ bot : HTT";
by (fast_tac (term_cs addDs [XH_to_D HTTXH]) 1);
qed "HTT_bot";
Goal "true : HTT";
by (fast_tac (term_cs addIs [XH_to_I HTTXH]) 1);
qed "HTT_true";
Goal "false : HTT";
by (fast_tac (term_cs addIs [XH_to_I HTTXH]) 1);
qed "HTT_false";
Goal "<a,b> : HTT <-> a : HTT & b : HTT";
by (rtac (HTTXH RS iff_trans) 1);
by (fast_tac term_cs 1);
qed "HTT_pair";
Goal "lam x. f(x) : HTT <-> (ALL x. f(x) : HTT)";
by (rtac (HTTXH RS iff_trans) 1);
by (simp_tac term_ss 1);
by (safe_tac term_cs);
by (asm_simp_tac term_ss 1);
by (fast_tac term_cs 1);
qed "HTT_lam";
local
val raw_HTTrews = [HTT_bot,HTT_true,HTT_false,HTT_pair,HTT_lam];
fun mk_thm s = prove_goalw Hered.thy data_defs s (fn _ =>
[simp_tac (term_ss addsimps raw_HTTrews) 1]);
in
val HTT_rews = raw_HTTrews @
map mk_thm ["one : HTT",
"inl(a) : HTT <-> a : HTT",
"inr(b) : HTT <-> b : HTT",
"zero : HTT",
"succ(n) : HTT <-> n : HTT",
"[] : HTT",
"x$xs : HTT <-> x : HTT & xs : HTT"];
end;
val HTT_Is = HTT_rews @ (HTT_rews RL [iffD2]);
(*** Coinduction for HTT ***)
val prems = goal Hered.thy "[| t : R; R <= HTTgen(R) |] ==> t : HTT";
by (rtac (HTT_def RS def_coinduct) 1);
by (REPEAT (ares_tac prems 1));
qed "HTT_coinduct";
fun HTT_coinduct_tac s i = res_inst_tac [("R",s)] HTT_coinduct i;
val prems = goal Hered.thy
"[| t : R; R <= HTTgen(lfp(%x. HTTgen(x) Un R Un HTT)) |] ==> t : HTT";
by (rtac (HTTgen_mono RSN(3,HTT_def RS def_coinduct3)) 1);
by (REPEAT (ares_tac prems 1));
qed "HTT_coinduct3";
val HTT_coinduct3_raw = rewrite_rule [HTTgen_def] HTT_coinduct3;
fun HTT_coinduct3_tac s i = res_inst_tac [("R",s)] HTT_coinduct3 i;
val HTTgenIs = map (mk_genIs Hered.thy data_defs HTTgenXH HTTgen_mono)
["true : HTTgen(R)",
"false : HTTgen(R)",
"[| a : R; b : R |] ==> <a,b> : HTTgen(R)",
"[| !!x. b(x) : R |] ==> lam x. b(x) : HTTgen(R)",
"one : HTTgen(R)",
"a : lfp(%x. HTTgen(x) Un R Un HTT) ==> \
\ inl(a) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
"b : lfp(%x. HTTgen(x) Un R Un HTT) ==> \
\ inr(b) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
"zero : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
"n : lfp(%x. HTTgen(x) Un R Un HTT) ==> \
\ succ(n) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
"[] : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
"[| h : lfp(%x. HTTgen(x) Un R Un HTT); t : lfp(%x. HTTgen(x) Un R Un HTT) |] ==>\
\ h$t : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"];
(*** Formation Rules for Types ***)
Goal "Unit <= HTT";
by (simp_tac (CCL_ss addsimps ([subsetXH,UnitXH] @ HTT_rews)) 1);
qed "UnitF";
Goal "Bool <= HTT";
by (simp_tac (CCL_ss addsimps ([subsetXH,BoolXH] @ HTT_rews)) 1);
by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
qed "BoolF";
val prems = goal Hered.thy "[| A <= HTT; B <= HTT |] ==> A + B <= HTT";
by (simp_tac (CCL_ss addsimps ([subsetXH,PlusXH] @ HTT_rews)) 1);
by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
qed "PlusF";
val prems = goal Hered.thy
"[| A <= HTT; !!x. x:A ==> B(x) <= HTT |] ==> SUM x:A. B(x) <= HTT";
by (simp_tac (CCL_ss addsimps ([subsetXH,SgXH] @ HTT_rews)) 1);
by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
qed "SigmaF";
(*** Formation Rules for Recursive types - using coinduction these only need ***)
(*** exhaution rule for type-former ***)
(*Proof by induction - needs induction rule for type*)
Goal "Nat <= HTT";
by (simp_tac (term_ss addsimps [subsetXH]) 1);
by (safe_tac set_cs);
by (etac Nat_ind 1);
by (ALLGOALS (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD]))));
val NatF = result();
Goal "Nat <= HTT";
by (safe_tac set_cs);
by (etac HTT_coinduct3 1);
by (fast_tac (set_cs addIs HTTgenIs
addSEs [HTTgen_mono RS ci3_RI] addEs [XH_to_E NatXH]) 1);
qed "NatF";
val [prem] = goal Hered.thy "A <= HTT ==> List(A) <= HTT";
by (safe_tac set_cs);
by (etac HTT_coinduct3 1);
by (fast_tac (set_cs addSIs HTTgenIs
addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)]
addEs [XH_to_E ListXH]) 1);
qed "ListF";
val [prem] = goal Hered.thy "A <= HTT ==> Lists(A) <= HTT";
by (safe_tac set_cs);
by (etac HTT_coinduct3 1);
by (fast_tac (set_cs addSIs HTTgenIs
addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)]
addEs [XH_to_E ListsXH]) 1);
qed "ListsF";
val [prem] = goal Hered.thy "A <= HTT ==> ILists(A) <= HTT";
by (safe_tac set_cs);
by (etac HTT_coinduct3 1);
by (fast_tac (set_cs addSIs HTTgenIs
addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)]
addEs [XH_to_E IListsXH]) 1);
qed "IListsF";
(*** A possible use for this predicate is proving equality from pre-order ***)
(*** but it seems as easy (and more general) to do this directly by coinduction ***)
(*
val prems = goal Hered.thy "[| t : HTT; t [= u |] ==> u [= t";
by (po_coinduct_tac "{p. EX a b. p=<a,b> & b : HTT & b [= a}" 1);
by (fast_tac (ccl_cs addIs prems) 1);
by (safe_tac ccl_cs);
by (dtac (poXH RS iffD1) 1);
by (safe_tac (set_cs addSEs [HTT_bot RS notE]));
by (REPEAT_SOME (rtac (POgenXH RS iffD2) ORELSE' etac rev_mp));
by (ALLGOALS (simp_tac (term_ss addsimps HTT_rews)));
by (ALLGOALS (fast_tac ccl_cs));
qed "HTT_po_op";
val prems = goal Hered.thy "[| t : HTT; t [= u |] ==> t = u";
by (REPEAT (ares_tac (prems @ [conjI RS (eq_iff RS iffD2),HTT_po_op]) 1));
qed "HTT_po_eq";
*)