src/CTT/Arith.thy
changeset 39159 0dec18004e75
parent 36319 8feb2c4bef1a
child 58318 f95754ca7082
     1.1 --- a/src/CTT/Arith.thy	Mon Sep 06 19:11:01 2010 +0200
     1.2 +++ b/src/CTT/Arith.thy	Mon Sep 06 19:13:10 2010 +0200
     1.3 @@ -82,12 +82,12 @@
     1.4  
     1.5  lemma mult_typing: "[| a:N;  b:N |] ==> a #* b : N"
     1.6  apply (unfold arith_defs)
     1.7 -apply (tactic {* typechk_tac [thm "add_typing"] *})
     1.8 +apply (tactic {* typechk_tac [@{thm add_typing}] *})
     1.9  done
    1.10  
    1.11  lemma mult_typingL: "[| a=c:N;  b=d:N |] ==> a #* b = c #* d : N"
    1.12  apply (unfold arith_defs)
    1.13 -apply (tactic {* equal_tac [thm "add_typingL"] *})
    1.14 +apply (tactic {* equal_tac [@{thm add_typingL}] *})
    1.15  done
    1.16  
    1.17  (*computation for mult: 0 and successor cases*)
    1.18 @@ -159,19 +159,19 @@
    1.19  
    1.20  structure Arith_simp_data: TSIMP_DATA =
    1.21    struct
    1.22 -  val refl              = thm "refl_elem"
    1.23 -  val sym               = thm "sym_elem"
    1.24 -  val trans             = thm "trans_elem"
    1.25 -  val refl_red          = thm "refl_red"
    1.26 -  val trans_red         = thm "trans_red"
    1.27 -  val red_if_equal      = thm "red_if_equal"
    1.28 -  val default_rls       = thms "arithC_rls" @ thms "comp_rls"
    1.29 -  val routine_tac       = routine_tac (thms "arith_typing_rls" @ thms "routine_rls")
    1.30 +  val refl              = @{thm refl_elem}
    1.31 +  val sym               = @{thm sym_elem}
    1.32 +  val trans             = @{thm trans_elem}
    1.33 +  val refl_red          = @{thm refl_red}
    1.34 +  val trans_red         = @{thm trans_red}
    1.35 +  val red_if_equal      = @{thm red_if_equal}
    1.36 +  val default_rls       = @{thms arithC_rls} @ @{thms comp_rls}
    1.37 +  val routine_tac       = routine_tac (@{thms arith_typing_rls} @ @{thms routine_rls})
    1.38    end
    1.39  
    1.40  structure Arith_simp = TSimpFun (Arith_simp_data)
    1.41  
    1.42 -local val congr_rls = thms "congr_rls" in
    1.43 +local val congr_rls = @{thms congr_rls} in
    1.44  
    1.45  fun arith_rew_tac prems = make_rew_tac
    1.46      (Arith_simp.norm_tac(congr_rls, prems))
    1.47 @@ -271,7 +271,7 @@
    1.48  (*Solves first 0 goal, simplifies others.  Two sugbgoals remain.
    1.49    Both follow by rewriting, (2) using quantified induction hyp*)
    1.50  apply (tactic "intr_tac []") (*strips remaining PRODs*)
    1.51 -apply (tactic {* hyp_arith_rew_tac [thm "add_0_right"] *})
    1.52 +apply (tactic {* hyp_arith_rew_tac [@{thm add_0_right}] *})
    1.53  apply assumption
    1.54  done
    1.55  
    1.56 @@ -303,7 +303,7 @@
    1.57  
    1.58  lemma absdiff_self_eq_0: "a:N ==> a |-| a = 0 : N"
    1.59  apply (unfold absdiff_def)
    1.60 -apply (tactic {* arith_rew_tac [thm "diff_self_eq_0"] *})
    1.61 +apply (tactic {* arith_rew_tac [@{thm diff_self_eq_0}] *})
    1.62  done
    1.63  
    1.64  lemma absdiffC0: "a:N ==> 0 |-| a = a : N"
    1.65 @@ -321,7 +321,7 @@
    1.66  lemma absdiff_commute: "[| a:N;  b:N |] ==> a |-| b = b |-| a : N"
    1.67  apply (unfold absdiff_def)
    1.68  apply (rule add_commute)
    1.69 -apply (tactic {* typechk_tac [thm "diff_typing"] *})
    1.70 +apply (tactic {* typechk_tac [@{thm diff_typing}] *})
    1.71  done
    1.72  
    1.73  (*If a+b=0 then a=0.   Surprisingly tedious*)
    1.74 @@ -332,7 +332,7 @@
    1.75  apply (tactic "intr_tac []") (*strips remaining PRODs*)
    1.76  apply (rule_tac [2] zero_ne_succ [THEN FE])
    1.77  apply (erule_tac [3] EqE [THEN sym_elem])
    1.78 -apply (tactic {* typechk_tac [thm "add_typing"] *})
    1.79 +apply (tactic {* typechk_tac [@{thm add_typing}] *})
    1.80  done
    1.81  
    1.82  (*Version of above with the premise  a+b=0.
    1.83 @@ -354,7 +354,7 @@
    1.84  apply (rule_tac [2] add_eq0)
    1.85  apply (rule add_eq0)
    1.86  apply (rule_tac [6] add_commute [THEN trans_elem])
    1.87 -apply (tactic {* typechk_tac [thm "diff_typing"] *})
    1.88 +apply (tactic {* typechk_tac [@{thm diff_typing}] *})
    1.89  done
    1.90  
    1.91  (*if  a |-| b = 0  then  a = b
    1.92 @@ -366,7 +366,7 @@
    1.93  apply (tactic eqintr_tac)
    1.94  apply (rule add_diff_inverse [THEN sym_elem, THEN trans_elem])
    1.95  apply (rule_tac [3] EqE, tactic "assume_tac 3")
    1.96 -apply (tactic {* hyp_arith_rew_tac [thm "add_0_right"] *})
    1.97 +apply (tactic {* hyp_arith_rew_tac [@{thm add_0_right}] *})
    1.98  done
    1.99  
   1.100  
   1.101 @@ -376,12 +376,12 @@
   1.102  
   1.103  lemma mod_typing: "[| a:N;  b:N |] ==> a mod b : N"
   1.104  apply (unfold mod_def)
   1.105 -apply (tactic {* typechk_tac [thm "absdiff_typing"] *})
   1.106 +apply (tactic {* typechk_tac [@{thm absdiff_typing}] *})
   1.107  done
   1.108  
   1.109  lemma mod_typingL: "[| a=c:N;  b=d:N |] ==> a mod b = c mod d : N"
   1.110  apply (unfold mod_def)
   1.111 -apply (tactic {* equal_tac [thm "absdiff_typingL"] *})
   1.112 +apply (tactic {* equal_tac [@{thm absdiff_typingL}] *})
   1.113  done
   1.114  
   1.115  
   1.116 @@ -389,13 +389,13 @@
   1.117  
   1.118  lemma modC0: "b:N ==> 0 mod b = 0 : N"
   1.119  apply (unfold mod_def)
   1.120 -apply (tactic {* rew_tac [thm "absdiff_typing"] *})
   1.121 +apply (tactic {* rew_tac [@{thm absdiff_typing}] *})
   1.122  done
   1.123  
   1.124  lemma modC_succ:
   1.125  "[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y. succ(a mod b)) : N"
   1.126  apply (unfold mod_def)
   1.127 -apply (tactic {* rew_tac [thm "absdiff_typing"] *})
   1.128 +apply (tactic {* rew_tac [@{thm absdiff_typing}] *})
   1.129  done
   1.130  
   1.131  
   1.132 @@ -403,12 +403,12 @@
   1.133  
   1.134  lemma div_typing: "[| a:N;  b:N |] ==> a div b : N"
   1.135  apply (unfold div_def)
   1.136 -apply (tactic {* typechk_tac [thm "absdiff_typing", thm "mod_typing"] *})
   1.137 +apply (tactic {* typechk_tac [@{thm absdiff_typing}, @{thm mod_typing}] *})
   1.138  done
   1.139  
   1.140  lemma div_typingL: "[| a=c:N;  b=d:N |] ==> a div b = c div d : N"
   1.141  apply (unfold div_def)
   1.142 -apply (tactic {* equal_tac [thm "absdiff_typingL", thm "mod_typingL"] *})
   1.143 +apply (tactic {* equal_tac [@{thm absdiff_typingL}, @{thm mod_typingL}] *})
   1.144  done
   1.145  
   1.146  lemmas div_typing_rls = mod_typing div_typing absdiff_typing
   1.147 @@ -418,14 +418,14 @@
   1.148  
   1.149  lemma divC0: "b:N ==> 0 div b = 0 : N"
   1.150  apply (unfold div_def)
   1.151 -apply (tactic {* rew_tac [thm "mod_typing", thm "absdiff_typing"] *})
   1.152 +apply (tactic {* rew_tac [@{thm mod_typing}, @{thm absdiff_typing}] *})
   1.153  done
   1.154  
   1.155  lemma divC_succ:
   1.156   "[| a:N;  b:N |] ==> succ(a) div b =
   1.157       rec(succ(a) mod b, succ(a div b), %x y. a div b) : N"
   1.158  apply (unfold div_def)
   1.159 -apply (tactic {* rew_tac [thm "mod_typing"] *})
   1.160 +apply (tactic {* rew_tac [@{thm mod_typing}] *})
   1.161  done
   1.162  
   1.163  
   1.164 @@ -433,9 +433,9 @@
   1.165  lemma divC_succ2: "[| a:N;  b:N |] ==>
   1.166       succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), %x y. a div b) : N"
   1.167  apply (rule divC_succ [THEN trans_elem])
   1.168 -apply (tactic {* rew_tac (thms "div_typing_rls" @ [thm "modC_succ"]) *})
   1.169 +apply (tactic {* rew_tac (@{thms div_typing_rls} @ [@{thm modC_succ}]) *})
   1.170  apply (tactic {* NE_tac @{context} "succ (a mod b) |-|b" 1 *})
   1.171 -apply (tactic {* rew_tac [thm "mod_typing", thm "div_typing", thm "absdiff_typing"] *})
   1.172 +apply (tactic {* rew_tac [@{thm mod_typing}, @{thm div_typing}, @{thm absdiff_typing}] *})
   1.173  done
   1.174  
   1.175  (*for case analysis on whether a number is 0 or a successor*)
   1.176 @@ -451,19 +451,19 @@
   1.177  (*Main Result.  Holds when b is 0 since   a mod 0 = a     and    a div 0 = 0  *)
   1.178  lemma mod_div_equality: "[| a:N;  b:N |] ==> a mod b  #+  (a div b) #* b = a : N"
   1.179  apply (tactic {* NE_tac @{context} "a" 1 *})
   1.180 -apply (tactic {* arith_rew_tac (thms "div_typing_rls" @
   1.181 -  [thm "modC0", thm "modC_succ", thm "divC0", thm "divC_succ2"]) *})
   1.182 +apply (tactic {* arith_rew_tac (@{thms div_typing_rls} @
   1.183 +  [@{thm modC0}, @{thm modC_succ}, @{thm divC0}, @{thm divC_succ2}]) *})
   1.184  apply (rule EqE)
   1.185  (*case analysis on   succ(u mod b)|-|b  *)
   1.186  apply (rule_tac a1 = "succ (u mod b) |-| b" in iszero_decidable [THEN PlusE])
   1.187  apply (erule_tac [3] SumE)
   1.188 -apply (tactic {* hyp_arith_rew_tac (thms "div_typing_rls" @
   1.189 -  [thm "modC0", thm "modC_succ", thm "divC0", thm "divC_succ2"]) *})
   1.190 +apply (tactic {* hyp_arith_rew_tac (@{thms div_typing_rls} @
   1.191 +  [@{thm modC0}, @{thm modC_succ}, @{thm divC0}, @{thm divC_succ2}]) *})
   1.192  (*Replace one occurence of  b  by succ(u mod b).  Clumsy!*)
   1.193  apply (rule add_typingL [THEN trans_elem])
   1.194  apply (erule EqE [THEN absdiff_eq0, THEN sym_elem])
   1.195  apply (rule_tac [3] refl_elem)
   1.196 -apply (tactic {* hyp_arith_rew_tac (thms "div_typing_rls") *})
   1.197 +apply (tactic {* hyp_arith_rew_tac @{thms div_typing_rls} *})
   1.198  done
   1.199  
   1.200  end