src/HOL/Library/reflection.ML
changeset 29834 3237cfd177f3
parent 29805 a5da150bd0ab
child 30148 5d04b67a866e
     1.1 --- a/src/HOL/Library/reflection.ML	Sun Feb 08 11:59:26 2009 +0100
     1.2 +++ b/src/HOL/Library/reflection.ML	Mon Feb 09 11:19:44 2009 +0100
     1.3 @@ -86,6 +86,23 @@
     1.4  
     1.5  exception REIF of string;
     1.6  
     1.7 +fun dest_listT (Type ("List.list", [T])) = T;
     1.8 +
     1.9 +fun partition P [] = ([],[])
    1.10 +  | partition P (x::xs) = 
    1.11 +     let val (yes,no) = partition P xs
    1.12 +     in if P x then (x::yes,no) else (yes, x::no) end
    1.13 +
    1.14 +fun rearrange congs = 
    1.15 +let 
    1.16 + fun P (_, th) = 
    1.17 +  let val @{term "Trueprop"}$(Const ("op =",_) $l$_) = concl_of th
    1.18 +  in can dest_Var l end
    1.19 + val (yes,no) = partition P congs 
    1.20 + in no @ yes end
    1.21 +
    1.22 +fun genreif ctxt raw_eqs t =
    1.23 + let
    1.24  val bds = ref ([]: (typ * ((term list) * (term list))) list);
    1.25  
    1.26  fun index_of t = 
    1.27 @@ -106,8 +123,6 @@
    1.28      end)
    1.29   end;
    1.30  
    1.31 -fun dest_listT (Type ("List.list", [T])) = T;
    1.32 -
    1.33  fun decomp_genreif da cgns (t,ctxt) =
    1.34   let 
    1.35    val thy = ProofContext.theory_of ctxt 
    1.36 @@ -151,8 +166,6 @@
    1.37    end;
    1.38  
    1.39   (* looks for the atoms equation and instantiates it with the right number *)
    1.40 -
    1.41 -
    1.42  fun mk_decompatom eqs (t,ctxt) =
    1.43  let 
    1.44   val tT = fastype_of t
    1.45 @@ -229,8 +242,8 @@
    1.46    (* Generic reification procedure: *)
    1.47    (* creates all needed cong rules and then just uses the theorem synthesis *)
    1.48  
    1.49 -  fun mk_congs ctxt raw_eqs = 
    1.50 - let
    1.51 +fun mk_congs ctxt raw_eqs = 
    1.52 +let
    1.53    val fs = fold_rev (fn eq =>
    1.54  		     insert (op =) (eq |> prop_of |> HOLogic.dest_Trueprop 
    1.55  			 |> HOLogic.dest_eq |> fst |> strip_comb 
    1.56 @@ -257,23 +270,6 @@
    1.57  in ps ~~ (Variable.export ctxt' ctxt congs)
    1.58  end
    1.59  
    1.60 -fun partition P [] = ([],[])
    1.61 -  | partition P (x::xs) = 
    1.62 -     let val (yes,no) = partition P xs
    1.63 -     in if P x then (x::yes,no) else (yes, x::no) end
    1.64 -
    1.65 -fun rearrange congs = 
    1.66 -let 
    1.67 - fun P (_, th) = 
    1.68 -  let val @{term "Trueprop"}$(Const ("op =",_) $l$_) = concl_of th
    1.69 -  in can dest_Var l end
    1.70 - val (yes,no) = partition P congs 
    1.71 - in no @ yes end
    1.72 -
    1.73 -
    1.74 -
    1.75 -fun genreif ctxt raw_eqs t =
    1.76 - let 
    1.77    val congs = rearrange (mk_congs ctxt raw_eqs)
    1.78    val th = divide_and_conquer (decomp_genreif (mk_decompatom raw_eqs) congs) (t,ctxt)
    1.79    fun is_listVar (Var (_,t)) = can dest_listT t