miz3/Samples/luxury.ml

   1 horizon := 0;;
   2
   3 let SUC_INJ_1 = thm `;
   4   now
   5     now [1]
   6       let m n be num;
   7       now [2]
   8         assume mk_num (IND_SUC (dest_num m)) =
   9                mk_num (IND_SUC (dest_num n)) [3];
  10         now [4]
  11           let p be num;
  12           NUM_REP (dest_num p) [5]
  13             by REWRITE_TAC[fst num_tydef; snd num_tydef] ;
  14           thus NUM_REP (IND_SUC (dest_num p))
  15             by MATCH_MP_TAC (CONJUNCT2 NUM_REP_RULES) from 5;
  16         end;
  17         !p. NUM_REP (IND_SUC (dest_num p)) [6] by GEN_TAC from 4;
  18         now [7]
  19           assume !p. dest_num (mk_num (IND_SUC (dest_num p))) =
  20                      IND_SUC (dest_num p) [8];
  21           mk_num (dest_num m) = mk_num (dest_num n) ==> m = n [9]
  22             by REWRITE_TAC[fst num_tydef];
  23           dest_num m = dest_num n ==> m = n [10]
  24             by DISCH_THEN(MP_TAC o AP_TERM (parse_term "mk_num")) from 9;
  25           thus dest_num (mk_num (IND_SUC (dest_num m))) =
  26                dest_num (mk_num (IND_SUC (dest_num n)))
  27                ==> m = n by ASM_REWRITE_TAC[IND_SUC_INJ],8 from 10;
  28         end;
  29         (!p. dest_num (mk_num (IND_SUC (dest_num p))) =
  30                IND_SUC (dest_num p))
  31           ==> dest_num (mk_num (IND_SUC (dest_num m))) =
  32               dest_num (mk_num (IND_SUC (dest_num n)))
  33           ==> m = n [11] by DISCH_TAC from 7;
  34         (!p. NUM_REP (IND_SUC (dest_num p)))
  35           ==> dest_num (mk_num (IND_SUC (dest_num m))) =
  36               dest_num (mk_num (IND_SUC (dest_num n)))
  37           ==> m = n [12] by REWRITE_TAC[fst num_tydef; snd num_tydef] from 11;
  38         dest_num (mk_num (IND_SUC (dest_num m))) =
  39           dest_num (mk_num (IND_SUC (dest_num n)))
  40           ==> m = n [13]
  41             by SUBGOAL_THEN (parse_term "!p. NUM_REP (IND_SUC (dest_num p))")
  42               MP_TAC from 6,12;
  43         thus m = n
  44           by POP_ASSUM(MP_TAC o AP_TERM (parse_term "dest_num")),3 from 13;
  45       end;
  46       mk_num (IND_SUC (dest_num m)) = mk_num (IND_SUC (dest_num n))
  47         ==> m = n [14] by DISCH_TAC from 2;
  48       now [15]
  49         assume m = n [16];
  50         thus mk_num (IND_SUC (dest_num m)) =
  51              mk_num (IND_SUC (dest_num n)) by ASM_REWRITE_TAC[],16;
  52       end;
  53       m = n
  54         ==> mk_num (IND_SUC (dest_num m)) =
  55             mk_num (IND_SUC (dest_num n)) [17] by DISCH_TAC from 15;
  56       mk_num (IND_SUC (dest_num m)) = mk_num (IND_SUC (dest_num n)) <=>
  57         m = n [18] by EQ_TAC from 14,17;
  58       thus SUC m = SUC n <=> m = n by REWRITE_TAC[SUC_DEF] from 18;
  59     end;
  60     thus !m n. SUC m = SUC n <=> m = n by REPEAT GEN_TAC from 1;
  61   end;
  62 `;;
  63
  64 let SUC_INJ_2 = thm `;
  65   !m n. SUC m = SUC n <=> m = n [1]
  66   proof
  67     let m n be num;
  68     mk_num (IND_SUC (dest_num m)) = mk_num (IND_SUC (dest_num n))
  69     ==> m = n [2]
  70     proof
  71       assume mk_num (IND_SUC (dest_num m)) =
  72              mk_num (IND_SUC (dest_num n)) [3];
  73       !p. NUM_REP (IND_SUC (dest_num p)) [4]
  74       proof
  75         let p be num;
  76         NUM_REP (dest_num p) [5]
  77           by REWRITE_TAC[fst num_tydef; snd num_tydef];
  78       qed by MATCH_MP_TAC (CONJUNCT2 NUM_REP_RULES) from 5;
  79       (!p. dest_num (mk_num (IND_SUC (dest_num p))) =
  80            IND_SUC (dest_num p))
  81       ==> dest_num (mk_num (IND_SUC (dest_num m))) =
  82           dest_num (mk_num (IND_SUC (dest_num n)))
  83       ==> m = n [6]
  84       proof
  85         assume !p. dest_num (mk_num (IND_SUC (dest_num p))) =
  86                    IND_SUC (dest_num p) [7];
  87         mk_num (dest_num m) = mk_num (dest_num n) ==> m = n [8]
  88           by REWRITE_TAC[fst num_tydef];
  89         dest_num m = dest_num n ==> m = n [9]
  90           by DISCH_THEN(MP_TAC o AP_TERM (parse_term "mk_num")) from 8;
  91       qed by ASM_REWRITE_TAC[IND_SUC_INJ],* from 9;
  92       (!p. NUM_REP (IND_SUC (dest_num p)))
  93       ==> dest_num (mk_num (IND_SUC (dest_num m))) =
  94           dest_num (mk_num (IND_SUC (dest_num n)))
  95       ==> m = n [10] by REWRITE_TAC[fst num_tydef; snd num_tydef] from 6;
  96       dest_num (mk_num (IND_SUC (dest_num m))) =
  97       dest_num (mk_num (IND_SUC (dest_num n)))
  98       ==> m = n [11]
  99         by SUBGOAL_THEN (parse_term "!p. NUM_REP (IND_SUC (dest_num p))")
 100           MP_TAC
 101         from 4,10;
 102     qed by POP_ASSUM(MP_TAC o AP_TERM (parse_term "dest_num")),3 from 11;
 103     m = n
 104     ==> mk_num (IND_SUC (dest_num m)) = mk_num (IND_SUC (dest_num n)) [12]
 105     proof
 106       assume m = n [13];
 107     qed by ASM_REWRITE_TAC[],*;
 108     mk_num (IND_SUC (dest_num m)) = mk_num (IND_SUC (dest_num n)) <=>
 109     m = n [14] by EQ_TAC from 2,12;
 110   qed by REWRITE_TAC[SUC_DEF] from 14;`;;
 111
 112 let num_INDUCTION_ = thm `;
 113   now [1]
 114     let P be num->bool;
 115     let n be num;
 116     assume P _0;
 117     assume !n. P n ==> P (SUC n);
 118     now [2]
 119       let i be ind;
 120       assume NUM_REP i;
 121       assume P (mk_num i);
 122       NUM_REP i [3] by ASM_REWRITE_TAC[],*;
 123       thus NUM_REP (IND_SUC i)
 124         by MATCH_MP_TAC(CONJUNCT2 NUM_REP_RULES) from 3;
 125     end;
 126     now [4]
 127       let i be ind;
 128       assume NUM_REP i;
 129       assume P (mk_num i);
 130       NUM_REP i [5] by FIRST_ASSUM MATCH_ACCEPT_TAC,*;
 131       dest_num (mk_num i) = i [6] by REWRITE_TAC[GSYM(snd num_tydef)] from 5;
 132       i = dest_num (mk_num i) [7] by CONV_TAC SYM_CONV from 6;
 133       mk_num (IND_SUC i) = mk_num (IND_SUC (dest_num (mk_num i))) [8]
 134         by REPEAT AP_TERM_TAC from 7;
 135       mk_num (IND_SUC i) = SUC (mk_num i) [9] by REWRITE_TAC[SUC_DEF] from 8;
 136       P (mk_num i) [10] by FIRST_ASSUM MATCH_ACCEPT_TAC,*;
 137       P (SUC (mk_num i)) [11] by FIRST_ASSUM MATCH_MP_TAC,* from 10;
 138       thus P (mk_num (IND_SUC i))
 139         by SUBGOAL_THEN (parse_term "mk_num(IND_SUC i) = SUC(mk_num i)")
 140            SUBST1_TAC
 141         from 9,11;
 142     end;
 143     !i. NUM_REP i /\ P (mk_num i)
 144           ==> NUM_REP (IND_SUC i) /\ P (mk_num (IND_SUC i)) [12]
 145       by REPEAT STRIP_TAC from 2,4;
 146     (NUM_REP (dest_num n)
 147        ==> NUM_REP (dest_num n) /\ P (mk_num (dest_num n)))
 148       ==> P n [13] by REWRITE_TAC[fst num_tydef; snd num_tydef];
 149     (!a. NUM_REP a ==> NUM_REP a /\ P (mk_num a)) ==> P n [14]
 150       by DISCH_THEN(MP_TAC o SPEC (parse_term "dest_num n")) from 13;
 151     ((!i. NUM_REP i /\ P (mk_num i)
 152             ==> NUM_REP (IND_SUC i) /\ P (mk_num (IND_SUC i)))
 153        ==> (!a. NUM_REP a ==> NUM_REP a /\ P (mk_num a)))
 154       ==> P n [15]
 155       by W(C SUBGOAL_THEN (fun t -> REWRITE_TAC[t]) o funpow 2 lhand o snd)
 156       from 12,14;
 157     ((\i. NUM_REP i /\ P (mk_num i)) IND_0 /\
 158        (!i. (\i. NUM_REP i /\ P (mk_num i)) i
 159             ==> (\i. NUM_REP i /\ P (mk_num i)) (IND_SUC i))
 160        ==> (!a. NUM_REP a ==> (\i. NUM_REP i /\ P (mk_num i)) a))
 161       ==> P n [16] by ASM_REWRITE_TAC[GSYM ZERO_DEF; NUM_REP_RULES],* from 15;
 162     thus P n by MP_TAC (SPEC (parse_term
 163       "\\i. NUM_REP i /\\ P(mk_num i):bool") NUM_REP_INDUCT) from 16;
 164   end;
 165   thus !P. P(_0) /\ (!n. P(n) ==> P(SUC n)) ==> !n. P n
 166     by REPEAT STRIP_TAC from 1;
 167 `;;
 168
 169 let num_RECURSION_STD = thm `;
 170   !e:Z f. ?fn. (fn 0 = e) /\ (!n. fn (SUC n) = f n (fn n))
 171   proof
 172     !e:Z f. ?fn. fn 0 = e /\ (!n. fn (SUC n) = f n (fn n)) [1]
 173     proof
 174       let e be Z;
 175       let f be num->Z->Z;
 176       (?fn. fn 0 = e /\ (!n. fn (SUC n) = (\z n. f n z) (fn n) n))
 177         ==> (?fn. fn 0 = e /\ (!n. fn (SUC n) = f n (fn n))) [2]
 178         by REWRITE_TAC[];
 179     qed by MP_TAC(ISPECL [(parse_term "e:Z");
 180       (parse_term "(\\z n. (f:num->Z->Z) n z)")] num_RECURSION) from 2;
 181   qed by REPEAT GEN_TAC from 1;
 182 `;;
 183