src/CCL/Hered.ML
changeset 0 a5a9c433f639
child 8 c3d2c6dcf3f0
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/CCL/Hered.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,196 @@
     1.4 +(*  Title: 	CCL/hered
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Martin Coen, Cambridge University Computer Laboratory
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +
     1.9 +For hered.thy.
    1.10 +*)
    1.11 +
    1.12 +open Hered;
    1.13 +
    1.14 +fun type_of_terms (Const("Trueprop",_) $ (Const("op =",(Type ("fun", [t,_])))$_$_)) = t;
    1.15 +
    1.16 +val cong_rls = ccl_mk_congs Hered.thy  ["HTTgen"];
    1.17 +
    1.18 +(*** Hereditary Termination ***)
    1.19 +
    1.20 +goalw Hered.thy [HTTgen_def]  "mono(%X.HTTgen(X))";
    1.21 +br monoI 1;
    1.22 +by (fast_tac set_cs 1);
    1.23 +val HTTgen_mono = result();
    1.24 +
    1.25 +goalw Hered.thy [HTTgen_def]
    1.26 +  "t : HTTgen(A) <-> t=true | t=false | (EX a b.t=<a,b> & a : A & b : A) | \
    1.27 +\                                       (EX f.t=lam x.f(x) & (ALL x.f(x) : A))";
    1.28 +by (fast_tac set_cs 1);
    1.29 +val HTTgenXH = result();
    1.30 +
    1.31 +goal Hered.thy
    1.32 +  "t : HTT <-> t=true | t=false | (EX a b.t=<a,b> & a : HTT & b : HTT) | \
    1.33 +\                                  (EX f.t=lam x.f(x) & (ALL x.f(x) : HTT))";
    1.34 +br (rewrite_rule [HTTgen_def] 
    1.35 +                 (HTTgen_mono RS (HTT_def RS def_gfp_Tarski) RS XHlemma1)) 1;
    1.36 +by (fast_tac set_cs 1);
    1.37 +val HTTXH = result();
    1.38 +
    1.39 +(*** Introduction Rules for HTT ***)
    1.40 +
    1.41 +goal Hered.thy "~ bot : HTT";
    1.42 +by (fast_tac (term_cs addDs [XH_to_D HTTXH]) 1);
    1.43 +val HTT_bot = result();
    1.44 +
    1.45 +goal Hered.thy "true : HTT";
    1.46 +by (fast_tac (term_cs addIs [XH_to_I HTTXH]) 1);
    1.47 +val HTT_true = result();
    1.48 +
    1.49 +goal Hered.thy "false : HTT";
    1.50 +by (fast_tac (term_cs addIs [XH_to_I HTTXH]) 1);
    1.51 +val HTT_false = result();
    1.52 +
    1.53 +goal Hered.thy "<a,b> : HTT <->  a : HTT  & b : HTT";
    1.54 +br (HTTXH RS iff_trans) 1;
    1.55 +by (fast_tac term_cs 1);
    1.56 +val HTT_pair = result();
    1.57 +
    1.58 +goal Hered.thy "lam x.f(x) : HTT <-> (ALL x. f(x) : HTT)";
    1.59 +br (HTTXH RS iff_trans) 1;
    1.60 +by (SIMP_TAC term_ss 1);
    1.61 +by (safe_tac term_cs);
    1.62 +by (ASM_SIMP_TAC term_ss 1);
    1.63 +by (fast_tac term_cs 1);
    1.64 +val HTT_lam = result();
    1.65 +
    1.66 +local
    1.67 +  val raw_HTTrews = [HTT_bot,HTT_true,HTT_false,HTT_pair,HTT_lam];
    1.68 +  fun mk_thm s = prove_goalw Hered.thy data_defs s (fn _ => 
    1.69 +                  [SIMP_TAC (term_ss addrews raw_HTTrews) 1]);
    1.70 +in
    1.71 +  val HTT_rews = raw_HTTrews @
    1.72 +               map mk_thm ["one : HTT",
    1.73 +                           "inl(a) : HTT <-> a : HTT",
    1.74 +                           "inr(b) : HTT <-> b : HTT",
    1.75 +                           "zero : HTT",
    1.76 +                           "succ(n) : HTT <-> n : HTT",
    1.77 +                           "[] : HTT",
    1.78 +                           "x.xs : HTT <-> x : HTT & xs : HTT"];
    1.79 +end;
    1.80 +
    1.81 +val HTT_Is = HTT_rews @ (HTT_rews RL [iffD2]);
    1.82 +
    1.83 +(*** Coinduction for HTT ***)
    1.84 +
    1.85 +val prems = goal Hered.thy "[|  t : R;  R <= HTTgen(R) |] ==> t : HTT";
    1.86 +br (HTT_def RS def_coinduct) 1;
    1.87 +by (REPEAT (ares_tac prems 1));
    1.88 +val HTT_coinduct = result();
    1.89 +
    1.90 +fun HTT_coinduct_tac s i = res_inst_tac [("R",s)] HTT_coinduct i;
    1.91 +
    1.92 +val prems = goal Hered.thy 
    1.93 +    "[|  t : R;   R <= HTTgen(lfp(%x. HTTgen(x) Un R Un HTT)) |] ==> t : HTT";
    1.94 +br (HTTgen_mono RSN(3,HTT_def RS def_coinduct3)) 1;
    1.95 +by (REPEAT (ares_tac prems 1));
    1.96 +val HTT_coinduct3 = result();
    1.97 +val HTT_coinduct3_raw = rewrite_rule [HTTgen_def] HTT_coinduct3;
    1.98 +
    1.99 +fun HTT_coinduct3_tac s i = res_inst_tac [("R",s)] HTT_coinduct3 i;
   1.100 +
   1.101 +val HTTgenIs = map (mk_genIs Hered.thy data_defs HTTgenXH HTTgen_mono)
   1.102 +       ["true : HTTgen(R)",
   1.103 +        "false : HTTgen(R)",
   1.104 +        "[| a : R;  b : R |] ==> <a,b> : HTTgen(R)",
   1.105 +        "[| !!x. b(x) : R |] ==> lam x.b(x) : HTTgen(R)",
   1.106 +        "one : HTTgen(R)",
   1.107 +        "a : lfp(%x. HTTgen(x) Un R Un HTT) ==> \
   1.108 +\                         inl(a) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
   1.109 +        "b : lfp(%x. HTTgen(x) Un R Un HTT) ==> \
   1.110 +\                         inr(b) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
   1.111 +        "zero : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
   1.112 +        "n : lfp(%x. HTTgen(x) Un R Un HTT) ==> \
   1.113 +\                         succ(n) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
   1.114 +        "[] : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
   1.115 +        "[| h : lfp(%x. HTTgen(x) Un R Un HTT); t : lfp(%x. HTTgen(x) Un R Un HTT) |] ==>\
   1.116 +\                         h.t : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"];
   1.117 +
   1.118 +(*** Formation Rules for Types ***)
   1.119 +
   1.120 +goal Hered.thy "Unit <= HTT";
   1.121 +by (SIMP_TAC (CCL_ss addrews ([subsetXH,UnitXH] @ HTT_rews)) 1);
   1.122 +val UnitF = result();
   1.123 +
   1.124 +goal Hered.thy "Bool <= HTT";
   1.125 +by (SIMP_TAC (CCL_ss addrews ([subsetXH,BoolXH] @ HTT_rews)) 1);
   1.126 +by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
   1.127 +val BoolF = result();
   1.128 +
   1.129 +val prems = goal Hered.thy "[| A <= HTT;  B <= HTT |] ==> A + B  <= HTT";
   1.130 +by (SIMP_TAC (CCL_ss addrews ([subsetXH,PlusXH] @ HTT_rews)) 1);
   1.131 +by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
   1.132 +val PlusF = result();
   1.133 +
   1.134 +val prems = goal Hered.thy 
   1.135 +     "[| A <= HTT;  !!x.x:A ==> B(x) <= HTT |] ==> SUM x:A.B(x) <= HTT";
   1.136 +by (SIMP_TAC (CCL_ss addrews ([subsetXH,SgXH] @ HTT_rews)) 1);
   1.137 +by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
   1.138 +val SigmaF = result();
   1.139 +
   1.140 +(*** Formation Rules for Recursive types - using coinduction these only need ***)
   1.141 +(***                                          exhaution rule for type-former ***)
   1.142 +
   1.143 +(*Proof by induction - needs induction rule for type*)
   1.144 +goal Hered.thy "Nat <= HTT";
   1.145 +by (SIMP_TAC (term_ss addrews [subsetXH]) 1);
   1.146 +by (safe_tac set_cs);
   1.147 +be Nat_ind 1;
   1.148 +by (ALLGOALS (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD]))));
   1.149 +val NatF = result();
   1.150 +
   1.151 +goal Hered.thy "Nat <= HTT";
   1.152 +by (safe_tac set_cs);
   1.153 +be HTT_coinduct3 1;
   1.154 +by (fast_tac (set_cs addIs HTTgenIs 
   1.155 +                 addSEs [HTTgen_mono RS ci3_RI] addEs [XH_to_E NatXH]) 1);
   1.156 +val NatF = result();
   1.157 +
   1.158 +val [prem] = goal Hered.thy "A <= HTT ==> List(A) <= HTT";
   1.159 +by (safe_tac set_cs);
   1.160 +be HTT_coinduct3 1;
   1.161 +by (fast_tac (set_cs addSIs HTTgenIs 
   1.162 +                 addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] 
   1.163 +                 addEs [XH_to_E ListXH]) 1);
   1.164 +val ListF = result();
   1.165 +
   1.166 +val [prem] = goal Hered.thy "A <= HTT ==> Lists(A) <= HTT";
   1.167 +by (safe_tac set_cs);
   1.168 +be HTT_coinduct3 1;
   1.169 +by (fast_tac (set_cs addSIs HTTgenIs 
   1.170 +                 addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] 
   1.171 +                 addEs [XH_to_E ListsXH]) 1);
   1.172 +val ListsF = result();
   1.173 +
   1.174 +val [prem] = goal Hered.thy "A <= HTT ==> ILists(A) <= HTT";
   1.175 +by (safe_tac set_cs);
   1.176 +be HTT_coinduct3 1;
   1.177 +by (fast_tac (set_cs addSIs HTTgenIs 
   1.178 +                 addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] 
   1.179 +                 addEs [XH_to_E IListsXH]) 1);
   1.180 +val IListsF = result();
   1.181 +
   1.182 +(*** A possible use for this predicate is proving equality from pre-order       ***)
   1.183 +(*** but it seems as easy (and more general) to do this directly by coinduction ***)
   1.184 +(*
   1.185 +val prems = goal Hered.thy "[| t : HTT;  t [= u |] ==> u [= t";
   1.186 +by (po_coinduct_tac "{p. EX a b.p=<a,b> & b : HTT & b [= a}" 1);
   1.187 +by (fast_tac (ccl_cs addIs prems) 1);
   1.188 +by (safe_tac ccl_cs);
   1.189 +bd (poXH RS iffD1) 1;
   1.190 +by (safe_tac (set_cs addSEs [HTT_bot RS notE]));
   1.191 +by (REPEAT_SOME (rtac (POgenXH RS iffD2) ORELSE' etac rev_mp));
   1.192 +by (ALLGOALS (SIMP_TAC (term_ss addrews HTT_rews)));
   1.193 +by (ALLGOALS (fast_tac ccl_cs));
   1.194 +val HTT_po_op = result();
   1.195 +
   1.196 +val prems = goal Hered.thy "[| t : HTT;  t [= u |] ==> t = u";
   1.197 +by (REPEAT (ares_tac (prems @ [conjI RS (eq_iff RS iffD2),HTT_po_op]) 1));
   1.198 +val HTT_po_eq = result();
   1.199 +*)