src/Pure/logic.ML
changeset 56245 84fc7dfa3cd4
parent 56244 3298b7a2795a
child 59787 6e2a20486897
     1.1 --- a/src/Pure/logic.ML	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/Pure/logic.ML	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -93,14 +93,14 @@
     1.4  
     1.5  (** all **)
     1.6  
     1.7 -fun all_const T = Const ("all", (T --> propT) --> propT);
     1.8 +fun all_const T = Const ("Pure.all", (T --> propT) --> propT);
     1.9  
    1.10  fun all v t = all_const (Term.fastype_of v) $ lambda v t;
    1.11  
    1.12 -fun is_all (Const ("all", _) $ Abs _) = true
    1.13 +fun is_all (Const ("Pure.all", _) $ Abs _) = true
    1.14    | is_all _ = false;
    1.15  
    1.16 -fun dest_all (Const ("all", _) $ Abs (abs as (_, T, _))) =
    1.17 +fun dest_all (Const ("Pure.all", _) $ Abs (abs as (_, T, _))) =
    1.18        let val (x, b) = Term.dest_abs abs  (*potentially slow*)
    1.19        in ((x, T), b) end
    1.20    | dest_all t = raise TERM ("dest_all", [t]);
    1.21 @@ -113,19 +113,19 @@
    1.22  
    1.23  fun mk_equals (t, u) =
    1.24    let val T = Term.fastype_of t
    1.25 -  in Const ("==", T --> T --> propT) $ t $ u end;
    1.26 +  in Const ("Pure.eq", T --> T --> propT) $ t $ u end;
    1.27  
    1.28 -fun dest_equals (Const ("==", _) $ t $ u) = (t, u)
    1.29 +fun dest_equals (Const ("Pure.eq", _) $ t $ u) = (t, u)
    1.30    | dest_equals t = raise TERM ("dest_equals", [t]);
    1.31  
    1.32  
    1.33  (** implies **)
    1.34  
    1.35 -val implies = Const ("==>", propT --> propT --> propT);
    1.36 +val implies = Const ("Pure.imp", propT --> propT --> propT);
    1.37  
    1.38  fun mk_implies (A, B) = implies $ A $ B;
    1.39  
    1.40 -fun dest_implies (Const ("==>", _) $ A $ B) = (A, B)
    1.41 +fun dest_implies (Const ("Pure.imp", _) $ A $ B) = (A, B)
    1.42    | dest_implies A = raise TERM ("dest_implies", [A]);
    1.43  
    1.44  
    1.45 @@ -136,28 +136,28 @@
    1.46    | list_implies (A::As, B) = implies $ A $ list_implies(As,B);
    1.47  
    1.48  (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
    1.49 -fun strip_imp_prems (Const("==>", _) $ A $ B) = A :: strip_imp_prems B
    1.50 +fun strip_imp_prems (Const("Pure.imp", _) $ A $ B) = A :: strip_imp_prems B
    1.51    | strip_imp_prems _ = [];
    1.52  
    1.53  (* A1==>...An==>B  goes to B, where B is not an implication *)
    1.54 -fun strip_imp_concl (Const("==>", _) $ A $ B) = strip_imp_concl B
    1.55 +fun strip_imp_concl (Const("Pure.imp", _) $ A $ B) = strip_imp_concl B
    1.56    | strip_imp_concl A = A : term;
    1.57  
    1.58  (*Strip and return premises: (i, [], A1==>...Ai==>B)
    1.59      goes to   ([Ai, A(i-1),...,A1] , B)         (REVERSED)
    1.60    if  i<0 or else i too big then raises  TERM*)
    1.61  fun strip_prems (0, As, B) = (As, B)
    1.62 -  | strip_prems (i, As, Const("==>", _) $ A $ B) =
    1.63 +  | strip_prems (i, As, Const("Pure.imp", _) $ A $ B) =
    1.64          strip_prems (i-1, A::As, B)
    1.65    | strip_prems (_, As, A) = raise TERM("strip_prems", A::As);
    1.66  
    1.67  (*Count premises -- quicker than (length o strip_prems) *)
    1.68 -fun count_prems (Const ("==>", _) $ _ $ B) = 1 + count_prems B
    1.69 +fun count_prems (Const ("Pure.imp", _) $ _ $ B) = 1 + count_prems B
    1.70    | count_prems _ = 0;
    1.71  
    1.72  (*Select Ai from A1 ==>...Ai==>B*)
    1.73 -fun nth_prem (1, Const ("==>", _) $ A $ _) = A
    1.74 -  | nth_prem (i, Const ("==>", _) $ _ $ B) = nth_prem (i - 1, B)
    1.75 +fun nth_prem (1, Const ("Pure.imp", _) $ A $ _) = A
    1.76 +  | nth_prem (i, Const ("Pure.imp", _) $ _ $ B) = nth_prem (i - 1, B)
    1.77    | nth_prem (_, A) = raise TERM ("nth_prem", [A]);
    1.78  
    1.79  (*strip a proof state (Horn clause):
    1.80 @@ -395,46 +395,46 @@
    1.81  
    1.82  fun lift_abs inc =
    1.83    let
    1.84 -    fun lift Ts (Const ("==>", _) $ _ $ B) t = lift Ts B t
    1.85 -      | lift Ts (Const ("all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t)
    1.86 +    fun lift Ts (Const ("Pure.imp", _) $ _ $ B) t = lift Ts B t
    1.87 +      | lift Ts (Const ("Pure.all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t)
    1.88        | lift Ts _ t = incr_indexes (rev Ts, inc) t;
    1.89    in lift [] end;
    1.90  
    1.91  fun lift_all inc =
    1.92    let
    1.93 -    fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t
    1.94 -      | lift Ts ((c as Const ("all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t)
    1.95 +    fun lift Ts ((c as Const ("Pure.imp", _)) $ A $ B) t = c $ A $ lift Ts B t
    1.96 +      | lift Ts ((c as Const ("Pure.all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t)
    1.97        | lift Ts _ t = incr_indexes (rev Ts, inc) t;
    1.98    in lift [] end;
    1.99  
   1.100  (*Strips assumptions in goal, yielding list of hypotheses.   *)
   1.101  fun strip_assums_hyp B =
   1.102    let
   1.103 -    fun strip Hs (Const ("==>", _) $ H $ B) = strip (H :: Hs) B
   1.104 -      | strip Hs (Const ("all", _) $ Abs (a, T, t)) =
   1.105 +    fun strip Hs (Const ("Pure.imp", _) $ H $ B) = strip (H :: Hs) B
   1.106 +      | strip Hs (Const ("Pure.all", _) $ Abs (a, T, t)) =
   1.107            strip (map (incr_boundvars 1) Hs) t
   1.108        | strip Hs B = rev Hs
   1.109    in strip [] B end;
   1.110  
   1.111  (*Strips assumptions in goal, yielding conclusion.   *)
   1.112 -fun strip_assums_concl (Const("==>", _) $ H $ B) = strip_assums_concl B
   1.113 -  | strip_assums_concl (Const("all",_)$Abs(a,T,t)) = strip_assums_concl t
   1.114 +fun strip_assums_concl (Const("Pure.imp", _) $ H $ B) = strip_assums_concl B
   1.115 +  | strip_assums_concl (Const("Pure.all",_)$Abs(a,T,t)) = strip_assums_concl t
   1.116    | strip_assums_concl B = B;
   1.117  
   1.118  (*Make a list of all the parameters in a subgoal, even if nested*)
   1.119 -fun strip_params (Const("==>", _) $ H $ B) = strip_params B
   1.120 -  | strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t
   1.121 +fun strip_params (Const("Pure.imp", _) $ H $ B) = strip_params B
   1.122 +  | strip_params (Const("Pure.all",_)$Abs(a,T,t)) = (a,T) :: strip_params t
   1.123    | strip_params B = [];
   1.124  
   1.125  (*test for nested meta connectives in prems*)
   1.126  val has_meta_prems =
   1.127    let
   1.128 -    fun is_meta (Const ("==", _) $ _ $ _) = true
   1.129 -      | is_meta (Const ("==>", _) $ _ $ _) = true
   1.130 -      | is_meta (Const ("all", _) $ _) = true
   1.131 +    fun is_meta (Const ("Pure.eq", _) $ _ $ _) = true
   1.132 +      | is_meta (Const ("Pure.imp", _) $ _ $ _) = true
   1.133 +      | is_meta (Const ("Pure.all", _) $ _) = true
   1.134        | is_meta _ = false;
   1.135 -    fun ex_meta (Const ("==>", _) $ A $ B) = is_meta A orelse ex_meta B
   1.136 -      | ex_meta (Const ("all", _) $ Abs (_, _, B)) = ex_meta B
   1.137 +    fun ex_meta (Const ("Pure.imp", _) $ A $ B) = is_meta A orelse ex_meta B
   1.138 +      | ex_meta (Const ("Pure.all", _) $ Abs (_, _, B)) = ex_meta B
   1.139        | ex_meta _ = false;
   1.140    in ex_meta end;
   1.141  
   1.142 @@ -444,10 +444,10 @@
   1.143  fun remove_params j n A =
   1.144      if j=0 andalso n<=0 then A  (*nothing left to do...*)
   1.145      else case A of
   1.146 -        Const("==>", _) $ H $ B =>
   1.147 +        Const("Pure.imp", _) $ H $ B =>
   1.148            if n=1 then                           (remove_params j (n-1) B)
   1.149            else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B)
   1.150 -      | Const("all",_)$Abs(a,T,t) => remove_params (j-1) n t
   1.151 +      | Const("Pure.all",_)$Abs(a,T,t) => remove_params (j-1) n t
   1.152        | _ => if n>0 then raise TERM("remove_params", [A])
   1.153               else A;
   1.154  
   1.155 @@ -460,9 +460,9 @@
   1.156      in list_all (vars, remove_params (length vars) n A) end;
   1.157  
   1.158  (*Makes parameters in a goal have the names supplied by the list cs.*)
   1.159 -fun list_rename_params cs (Const ("==>", _) $ A $ B) =
   1.160 +fun list_rename_params cs (Const ("Pure.imp", _) $ A $ B) =
   1.161        implies $ A $ list_rename_params cs B
   1.162 -  | list_rename_params (c :: cs) ((a as Const ("all", _)) $ Abs (_, T, t)) =
   1.163 +  | list_rename_params (c :: cs) ((a as Const ("Pure.all", _)) $ Abs (_, T, t)) =
   1.164        a $ Abs (c, T, list_rename_params cs t)
   1.165    | list_rename_params cs B = B;
   1.166  
   1.167 @@ -480,12 +480,12 @@
   1.168        Unless nasms<0, it can terminate the recursion early; that allows
   1.169    erule to work on assumptions of the form P==>Q.*)
   1.170  fun strip_assums_imp (0, Hs, B) = (Hs, B)  (*recursion terminated by nasms*)
   1.171 -  | strip_assums_imp (nasms, Hs, Const("==>", _) $ H $ B) =
   1.172 +  | strip_assums_imp (nasms, Hs, Const("Pure.imp", _) $ H $ B) =
   1.173        strip_assums_imp (nasms-1, H::Hs, B)
   1.174    | strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*)
   1.175  
   1.176  (*Strips OUTER parameters only.*)
   1.177 -fun strip_assums_all (params, Const("all",_)$Abs(a,T,t)) =
   1.178 +fun strip_assums_all (params, Const("Pure.all",_)$Abs(a,T,t)) =
   1.179        strip_assums_all ((a,T)::params, t)
   1.180    | strip_assums_all (params, B) = (params, B);
   1.181