diff -r 000000000000 -r a5a9c433f639 src/CCL/hered.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/CCL/hered.ML	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,196 @@
+(*  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;
+
+val cong_rls = ccl_mk_congs Hered.thy  ["HTTgen"];
+
+(*** Hereditary Termination ***)
+
+goalw Hered.thy [HTTgen_def]  "mono(%X.HTTgen(X))";
+br monoI 1;
+by (fast_tac set_cs 1);
+val HTTgen_mono = result();
+
+goalw Hered.thy [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);
+val HTTgenXH = result();
+
+goal Hered.thy
+  "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))";
+br (rewrite_rule [HTTgen_def] 
+                 (HTTgen_mono RS (HTT_def RS def_gfp_Tarski) RS XHlemma1)) 1;
+by (fast_tac set_cs 1);
+val HTTXH = result();
+
+(*** Introduction Rules for HTT ***)
+
+goal Hered.thy "~ bot : HTT";
+by (fast_tac (term_cs addDs [XH_to_D HTTXH]) 1);
+val HTT_bot = result();
+
+goal Hered.thy "true : HTT";
+by (fast_tac (term_cs addIs [XH_to_I HTTXH]) 1);
+val HTT_true = result();
+
+goal Hered.thy "false : HTT";
+by (fast_tac (term_cs addIs [XH_to_I HTTXH]) 1);
+val HTT_false = result();
+
+goal Hered.thy "<a,b> : HTT <->  a : HTT  & b : HTT";
+br (HTTXH RS iff_trans) 1;
+by (fast_tac term_cs 1);
+val HTT_pair = result();
+
+goal Hered.thy "lam x.f(x) : HTT <-> (ALL x. f(x) : HTT)";
+br (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);
+val HTT_lam = result();
+
+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 addrews 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";
+br (HTT_def RS def_coinduct) 1;
+by (REPEAT (ares_tac prems 1));
+val HTT_coinduct = result();
+
+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";
+br (HTTgen_mono RSN(3,HTT_def RS def_coinduct3)) 1;
+by (REPEAT (ares_tac prems 1));
+val HTT_coinduct3 = result();
+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 Hered.thy "Unit <= HTT";
+by (SIMP_TAC (CCL_ss addrews ([subsetXH,UnitXH] @ HTT_rews)) 1);
+val UnitF = result();
+
+goal Hered.thy "Bool <= HTT";
+by (SIMP_TAC (CCL_ss addrews ([subsetXH,BoolXH] @ HTT_rews)) 1);
+by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
+val BoolF = result();
+
+val prems = goal Hered.thy "[| A <= HTT;  B <= HTT |] ==> A + B  <= HTT";
+by (SIMP_TAC (CCL_ss addrews ([subsetXH,PlusXH] @ HTT_rews)) 1);
+by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
+val PlusF = result();
+
+val prems = goal Hered.thy 
+     "[| A <= HTT;  !!x.x:A ==> B(x) <= HTT |] ==> SUM x:A.B(x) <= HTT";
+by (SIMP_TAC (CCL_ss addrews ([subsetXH,SgXH] @ HTT_rews)) 1);
+by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
+val SigmaF = result();
+
+(*** Formation Rules for Recursive types - using coinduction these only need ***)
+(***                                          exhaution rule for type-former ***)
+
+(*Proof by induction - needs induction rule for type*)
+goal Hered.thy "Nat <= HTT";
+by (SIMP_TAC (term_ss addrews [subsetXH]) 1);
+by (safe_tac set_cs);
+be Nat_ind 1;
+by (ALLGOALS (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD]))));
+val NatF = result();
+
+goal Hered.thy "Nat <= HTT";
+by (safe_tac set_cs);
+be HTT_coinduct3 1;
+by (fast_tac (set_cs addIs HTTgenIs 
+                 addSEs [HTTgen_mono RS ci3_RI] addEs [XH_to_E NatXH]) 1);
+val NatF = result();
+
+val [prem] = goal Hered.thy "A <= HTT ==> List(A) <= HTT";
+by (safe_tac set_cs);
+be 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);
+val ListF = result();
+
+val [prem] = goal Hered.thy "A <= HTT ==> Lists(A) <= HTT";
+by (safe_tac set_cs);
+be 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);
+val ListsF = result();
+
+val [prem] = goal Hered.thy "A <= HTT ==> ILists(A) <= HTT";
+by (safe_tac set_cs);
+be 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);
+val IListsF = result();
+
+(*** 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);
+bd (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 addrews HTT_rews)));
+by (ALLGOALS (fast_tac ccl_cs));
+val HTT_po_op = result();
+
+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));
+val HTT_po_eq = result();
+*)