remove dead code
authorhuffman
Sat Oct 16 17:10:23 2010 -0700 (2010-10-16)
changeset 4002957e7f651fc70
parent 40028 9ee4e0ab2964
child 40030 9f8dcf6ef563
child 40035 a12d35795cb9
remove dead code
src/HOLCF/Tools/Domain/domain_theorems.ML
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Oct 16 17:09:57 2010 -0700
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Oct 16 17:10:23 2010 -0700
     1.3 @@ -5,8 +5,6 @@
     1.4  Proof generator for domain command.
     1.5  *)
     1.6  
     1.7 -val HOLCF_ss = @{simpset};
     1.8 -
     1.9  signature DOMAIN_THEOREMS =
    1.10  sig
    1.11    val comp_theorems :
    1.12 @@ -29,53 +27,6 @@
    1.13  fun trace s = if !trace_domain then tracing s else ();
    1.14  
    1.15  open HOLCF_Library;
    1.16 -infixr 0 ===>;
    1.17 -infix 0 == ; 
    1.18 -infix 1 ===;
    1.19 -infix 9 `   ;
    1.20 -
    1.21 -(* ----- general proof facilities ------------------------------------------- *)
    1.22 -
    1.23 -local
    1.24 -
    1.25 -fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)
    1.26 -  | map_typ f _ (TFree (x, S)) = TFree (x, map f S)
    1.27 -  | map_typ f _ (TVar (xi, S)) = TVar (xi, map f S);
    1.28 -
    1.29 -fun map_term f g h (Const (c, T)) = Const (h c, map_typ f g T)
    1.30 -  | map_term f g _ (Free (x, T)) = Free (x, map_typ f g T)
    1.31 -  | map_term f g _ (Var (xi, T)) = Var (xi, map_typ f g T)
    1.32 -  | map_term _ _ _ (t as Bound _) = t
    1.33 -  | map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t)
    1.34 -  | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
    1.35 -
    1.36 -in
    1.37 -
    1.38 -fun intern_term thy =
    1.39 -  map_term (Sign.intern_class thy) (Sign.intern_type thy) (Sign.intern_const thy);
    1.40 -
    1.41 -end;
    1.42 -
    1.43 -fun legacy_infer_term thy t =
    1.44 -  let val ctxt = ProofContext.set_mode ProofContext.mode_schematic (ProofContext.init_global thy)
    1.45 -  in singleton (Syntax.check_terms ctxt) (intern_term thy t) end;
    1.46 -
    1.47 -fun pg'' thy defs t tacs =
    1.48 -  let
    1.49 -    val t' = legacy_infer_term thy t;
    1.50 -    val asms = Logic.strip_imp_prems t';
    1.51 -    val prop = Logic.strip_imp_concl t';
    1.52 -    fun tac {prems, context} =
    1.53 -      rewrite_goals_tac defs THEN
    1.54 -      EVERY (tacs {prems = map (rewrite_rule defs) prems, context = context})
    1.55 -  in Goal.prove_global thy [] asms prop tac end;
    1.56 -
    1.57 -fun pg' thy defs t tacsf =
    1.58 -  let
    1.59 -    fun tacs {prems, context} =
    1.60 -      if null prems then tacsf context
    1.61 -      else cut_facts_tac prems 1 :: tacsf context;
    1.62 -  in pg'' thy defs t tacs end;
    1.63  
    1.64  (******************************************************************************)
    1.65  (***************************** proofs about take ******************************)
    1.66 @@ -135,17 +86,13 @@
    1.67      (dbinds ~~ take_consts ~~ constr_infos) thy
    1.68  end;
    1.69  
    1.70 -(* ----- general proofs ----------------------------------------------------- *)
    1.71 -
    1.72 -val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp}
    1.73 +(******************************************************************************)
    1.74 +(****************************** induction rules *******************************)
    1.75 +(******************************************************************************)
    1.76  
    1.77  val case_UU_allI =
    1.78      @{lemma "(!!x. x ~= UU ==> P x) ==> P UU ==> ALL x. P x" by metis};
    1.79  
    1.80 -(******************************************************************************)
    1.81 -(****************************** induction rules *******************************)
    1.82 -(******************************************************************************)
    1.83 -
    1.84  fun prove_induction
    1.85      (comp_dbind : binding)
    1.86      (constr_infos : Domain_Constructors.constr_info list)