author huffman Sat Oct 16 17:10:23 2010 -0700 (2010-10-16) changeset 40029 57e7f651fc70 parent 40028 9ee4e0ab2964 child 40030 9f8dcf6ef563 child 40035 a12d35795cb9
```     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)
```