Removed obsolete functions dealing with flex-flex constraints.
authorberghofe
Mon Oct 21 17:07:27 2002 +0200 (2002-10-21)
changeset 136593cf622f6b0b2
parent 13658 c9ad3e64ddcf
child 13660 e36798726ca4
Removed obsolete functions dealing with flex-flex constraints.
src/Pure/drule.ML
src/Pure/logic.ML
     1.1 --- a/src/Pure/drule.ML	Mon Oct 21 17:04:47 2002 +0200
     1.2 +++ b/src/Pure/drule.ML	Mon Oct 21 17:07:27 2002 +0200
     1.3 @@ -14,7 +14,6 @@
     1.4    val list_implies      : cterm list * cterm -> cterm
     1.5    val dest_implies      : cterm -> cterm * cterm
     1.6    val dest_equals       : cterm -> cterm * cterm
     1.7 -  val skip_flexpairs    : cterm -> cterm
     1.8    val strip_imp_prems   : cterm -> cterm list
     1.9    val strip_imp_concl   : cterm -> cterm
    1.10    val cprems_of         : thm -> cterm list
    1.11 @@ -69,7 +68,6 @@
    1.12    val swap_prems_eq     : thm
    1.13    val equal_abs_elim    : cterm  -> thm -> thm
    1.14    val equal_abs_elim_list: cterm list -> thm -> thm
    1.15 -  val flexpair_abs_elim_list: cterm list -> thm -> thm
    1.16    val asm_rl            : thm
    1.17    val cut_rl            : thm
    1.18    val revcut_rl         : thm
    1.19 @@ -159,13 +157,6 @@
    1.20        | _ => raise TERM ("dest_equals", [term_of ct]) ;
    1.21  
    1.22  
    1.23 -(*Discard flexflex pairs; return a cterm*)
    1.24 -fun skip_flexpairs ct =
    1.25 -    case term_of ct of
    1.26 -        (Const("==>", _) $ (Const("=?=",_)$_$_) $ _) =>
    1.27 -            skip_flexpairs (#2 (dest_implies ct))
    1.28 -      | _ => ct;
    1.29 -
    1.30  (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
    1.31  fun strip_imp_prems ct =
    1.32      let val (cA,cB) = dest_implies ct
    1.33 @@ -179,7 +170,7 @@
    1.34    | _ => ct;
    1.35  
    1.36  (*The premises of a theorem, as a cterm list*)
    1.37 -val cprems_of = strip_imp_prems o skip_flexpairs o cprop_of;
    1.38 +val cprems_of = strip_imp_prems o cprop_of;
    1.39  
    1.40  val proto_sign = Theory.sign_of ProtoPure.thy;
    1.41  
    1.42 @@ -403,16 +394,16 @@
    1.43    Similar code in type/freeze_thaw*)
    1.44  fun freeze_thaw th =
    1.45   let val fth = freezeT th
    1.46 -     val {prop,sign,...} = rep_thm fth
    1.47 +     val {prop, tpairs, sign, ...} = rep_thm fth
    1.48   in
    1.49 -   case term_vars prop of
    1.50 +   case foldr add_term_vars (prop :: Thm.terms_of_tpairs tpairs, []) of
    1.51         [] => (fth, fn x => x)
    1.52       | vars =>
    1.53           let fun newName (Var(ix,_), (pairs,used)) =
    1.54                     let val v = variant used (string_of_indexname ix)
    1.55                     in  ((ix,v)::pairs, v::used)  end;
    1.56 -             val (alist, _) = foldr newName
    1.57 -                                (vars, ([], add_term_names (prop, [])))
    1.58 +             val (alist, _) = foldr newName (vars, ([], foldr add_term_names
    1.59 +               (prop :: Thm.terms_of_tpairs tpairs, [])))
    1.60               fun mk_inst (Var(v,T)) =
    1.61                   (cterm_of sign (Var(v,T)),
    1.62                    cterm_of sign (Free(the (assoc(alist,v)), T)))
    1.63 @@ -791,27 +782,6 @@
    1.64  (*Calling equal_abs_elim with multiple terms*)
    1.65  fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) (rev cts, th);
    1.66  
    1.67 -local
    1.68 -  val alpha = TVar(("'a",0), [])     (*  type ?'a::{}  *)
    1.69 -  fun err th = raise THM("flexpair_inst: ", 0, [th])
    1.70 -  fun flexpair_inst def th =
    1.71 -    let val {prop = Const _ $ t $ u,  sign,...} = rep_thm th
    1.72 -        val cterm = cterm_of sign
    1.73 -        fun cvar a = cterm(Var((a,0),alpha))
    1.74 -        val def' = cterm_instantiate [(cvar"t", cterm t), (cvar"u", cterm u)]
    1.75 -                   def
    1.76 -    in  equal_elim def' th
    1.77 -    end
    1.78 -    handle THM _ => err th | Bind => err th
    1.79 -in
    1.80 -val flexpair_intr = flexpair_inst (symmetric ProtoPure.flexpair_def)
    1.81 -and flexpair_elim = flexpair_inst ProtoPure.flexpair_def
    1.82 -end;
    1.83 -
    1.84 -(*Version for flexflex pairs -- this supports lifting.*)
    1.85 -fun flexpair_abs_elim_list cts =
    1.86 -    flexpair_intr o equal_abs_elim_list cts o flexpair_elim;
    1.87 -
    1.88  
    1.89  (*** Goal (PROP A) <==> PROP A ***)
    1.90  
     2.1 --- a/src/Pure/logic.ML	Mon Oct 21 17:04:47 2002 +0200
     2.2 +++ b/src/Pure/logic.ML	Mon Oct 21 17:07:27 2002 +0200
     2.3 @@ -24,13 +24,7 @@
     2.4    val count_prems       : term * int -> int
     2.5    val mk_conjunction    : term * term -> term
     2.6    val mk_conjunction_list: term list -> term
     2.7 -  val mk_flexpair       : term * term -> term
     2.8 -  val dest_flexpair     : term -> term * term
     2.9 -  val list_flexpairs    : (term*term)list * term -> term
    2.10 -  val rule_of           : (term*term)list * term list * term -> term
    2.11 -  val strip_flexpairs   : term -> (term*term)list * term
    2.12 -  val skip_flexpairs    : term -> term
    2.13 -  val strip_horn        : term -> (term*term)list * term list * term
    2.14 +  val strip_horn        : term -> term list * term
    2.15    val mk_cond_defpair   : term list -> term * term -> string * term
    2.16    val mk_defpair        : term * term -> string * term
    2.17    val mk_type           : typ -> term
    2.18 @@ -118,6 +112,10 @@
    2.19  fun count_prems (Const("==>", _) $ A $ B, n) = count_prems (B,n+1)
    2.20    | count_prems (_,n) = n;
    2.21  
    2.22 +(*strip a proof state (Horn clause):
    2.23 +  B1 ==> ... Bn ==> C   goes to   ([B1, ..., Bn], C)    *)
    2.24 +fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
    2.25 +
    2.26  
    2.27  (** conjunction **)
    2.28  
    2.29 @@ -128,45 +126,6 @@
    2.30    | mk_conjunction_list ts = foldr1 mk_conjunction ts;
    2.31  
    2.32  
    2.33 -(** flex-flex constraints **)
    2.34 -
    2.35 -(*Make a constraint.*)
    2.36 -fun mk_flexpair(t,u) = flexpair(fastype_of t) $ t $ u;
    2.37 -
    2.38 -fun dest_flexpair (Const("=?=",_) $ t $ u)  =  (t,u)
    2.39 -  | dest_flexpair t = raise TERM("dest_flexpair", [t]);
    2.40 -
    2.41 -(*make flexflex antecedents: ( [(a1,b1),...,(an,bn)] , C )
    2.42 -    goes to (a1=?=b1) ==>...(an=?=bn)==>C *)
    2.43 -fun list_flexpairs ([], A) = A
    2.44 -  | list_flexpairs ((t,u)::pairs, A) =
    2.45 -        implies $ (mk_flexpair(t,u)) $ list_flexpairs(pairs,A);
    2.46 -
    2.47 -(*Make the object-rule tpairs==>As==>B   *)
    2.48 -fun rule_of (tpairs, As, B) = list_flexpairs(tpairs, list_implies(As, B));
    2.49 -
    2.50 -(*Remove and return flexflex pairs:
    2.51 -    (a1=?=b1)==>...(an=?=bn)==>C  to  ( [(a1,b1),...,(an,bn)] , C )
    2.52 -  [Tail recursive in order to return a pair of results] *)
    2.53 -fun strip_flex_aux (pairs, Const("==>", _) $ (Const("=?=",_)$t$u) $ C) =
    2.54 -        strip_flex_aux ((t,u)::pairs, C)
    2.55 -  | strip_flex_aux (pairs,C) = (rev pairs, C);
    2.56 -
    2.57 -fun strip_flexpairs A = strip_flex_aux([], A);
    2.58 -
    2.59 -(*Discard flexflex pairs*)
    2.60 -fun skip_flexpairs (Const("==>", _) $ (Const("=?=",_)$_$_) $ C) =
    2.61 -        skip_flexpairs C
    2.62 -  | skip_flexpairs C = C;
    2.63 -
    2.64 -(*strip a proof state (Horn clause):
    2.65 -   (a1==b1)==>...(am==bm)==>B1==>...Bn==>C
    2.66 -    goes to   ( [(a1,b1),...,(am,bm)] , [B1,...,Bn] , C)    *)
    2.67 -fun strip_horn A =
    2.68 -  let val (tpairs,horn) = strip_flexpairs A
    2.69 -  in  (tpairs, strip_imp_prems horn, strip_imp_concl horn)   end;
    2.70 -
    2.71 -
    2.72  (** definitions **)
    2.73  
    2.74  fun mk_cond_defpair As (lhs, rhs) =
    2.75 @@ -270,9 +229,8 @@
    2.76        | is_meta (Const ("==", _) $ _ $ _) = true
    2.77        | is_meta (Const ("all", _) $ _) = true
    2.78        | is_meta _ = false;
    2.79 -    val horn = skip_flexpairs prop;
    2.80    in
    2.81 -    (case strip_prems (i, [], horn) of
    2.82 +    (case strip_prems (i, [], prop) of
    2.83        (B :: _, _) => exists is_meta (strip_assums_hyp B)
    2.84      | _ => false) handle TERM _ => false
    2.85    end;