summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/MiniML/Generalize.ML

author | nipkow |

Fri, 24 Nov 2000 16:49:27 +0100 | |

changeset 10519 | ade64af4c57c |

parent 7036 | 895c7c1e56ba |

permissions | -rw-r--r-- |

hide many names from Datatype_Universe.

(* Title: HOL/MiniML/Generalize.ML ID: $Id$ Author: Wolfgang Naraschewski and Tobias Nipkow Copyright 1996 TU Muenchen *) AddSEs [equalityE]; Goal "free_tv A = free_tv B ==> gen A t = gen B t"; by (induct_tac "t" 1); by (ALLGOALS Asm_simp_tac); qed "gen_eq_on_free_tv"; Goal "(free_tv t) <= (free_tv sch) --> gen sch t = (mk_scheme t)"; by (induct_tac "t" 1); by (Asm_simp_tac 1); by (Simp_tac 1); by (Fast_tac 1); qed_spec_mp "gen_without_effect"; Addsimps [gen_without_effect]; Goal "free_tv (gen ($ S A) t) = free_tv t Int free_tv ($ S A)"; by (induct_tac "t" 1); by (Simp_tac 1); by (case_tac "nat : free_tv ($ S A)" 1); by (Asm_simp_tac 1); by (Fast_tac 1); by (Asm_simp_tac 1); by (Fast_tac 1); by (Asm_full_simp_tac 1); by (Fast_tac 1); qed "free_tv_gen"; Addsimps [free_tv_gen]; Goal "free_tv (gen ($ S A) t # $ S A) = free_tv ($ S A)"; by (Simp_tac 1); by (Fast_tac 1); qed "free_tv_gen_cons"; Addsimps [free_tv_gen_cons]; Goal "bound_tv (gen A t1) = (free_tv t1) - (free_tv A)"; by (induct_tac "t1" 1); by (Simp_tac 1); by (case_tac "nat : free_tv A" 1); by (Asm_simp_tac 1); by (Asm_simp_tac 1); by (Fast_tac 1); by (Asm_simp_tac 1); by (Fast_tac 1); qed "bound_tv_gen"; Addsimps [bound_tv_gen]; Goal "new_tv n t --> new_tv n (gen A t)"; by (induct_tac "t" 1); by Auto_tac; qed_spec_mp "new_tv_compatible_gen"; Goalw [gen_ML_def] "gen A t = gen_ML A t"; by (induct_tac "t" 1); by (simp_tac (simpset() addsimps [free_tv_ML_scheme_list]) 1); by (asm_simp_tac (simpset() addsimps [free_tv_ML_scheme_list]) 1); qed "gen_eq_gen_ML"; Goal "(free_tv S) Int ((free_tv t) - (free_tv A)) = {} \ \ --> gen ($ S A) ($ S t) = $ S (gen A t)"; by (induct_tac "t" 1); by (strip_tac 1); by (case_tac "nat:(free_tv A)" 1); by (Asm_simp_tac 1); by (Asm_full_simp_tac 1); by (subgoal_tac "nat ~: free_tv S" 1); by (Fast_tac 2); by (asm_full_simp_tac (simpset() addsimps [free_tv_subst,dom_def]) 1); by (cut_facts_tac [free_tv_app_subst_scheme_list] 1); by (Fast_tac 1); by (Asm_simp_tac 1); by (Blast_tac 1); qed_spec_mp "gen_subst_commutes"; Goal "free_tv(t::typ) <= free_tv(A) --> bound_typ_inst S (gen A t) = t"; by (induct_tac "t" 1); by (ALLGOALS Asm_simp_tac); by (Fast_tac 1); qed_spec_mp "bound_typ_inst_gen"; Addsimps [bound_typ_inst_gen]; Goalw [le_type_scheme_def,is_bound_typ_instance] "gen ($ S A) ($ S t) <= $ S (gen A t)"; by Safe_tac; by (rename_tac "R" 1); by (res_inst_tac [("x", "(%a. bound_typ_inst R (gen ($S A) (S a)))")] exI 1); by (induct_tac "t" 1); by (Simp_tac 1); by (Asm_simp_tac 1); qed "gen_bound_typ_instance"; Goalw [le_type_scheme_def,is_bound_typ_instance] "free_tv B <= free_tv A ==> gen A t <= gen B t"; by Safe_tac; by (rename_tac "S" 1); by (res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1); by (induct_tac "t" 1); by (Asm_simp_tac 1); by (Fast_tac 1); by (Asm_simp_tac 1); qed "free_tv_subset_gen_le"; Goalw [le_type_scheme_def,is_bound_typ_instance] "new_tv n A --> \ \ gen A t <= gen A ($ (%x. TVar (if x : free_tv A then x else n + x)) t)"; by (strip_tac 1); by (etac exE 1); by (hyp_subst_tac 1); by (res_inst_tac [("x","(%x. S (if n <= x then x - n else x))")] exI 1); by (induct_tac "t" 1); by (Simp_tac 1); by (case_tac "nat : free_tv A" 1); by (Asm_simp_tac 1); by (Asm_simp_tac 1); by (subgoal_tac "n <= n + nat" 1); by (forw_inst_tac [("t","A")] new_tv_le 1); by (assume_tac 1); by (dtac new_tv_not_free_tv 1); by (dtac new_tv_not_free_tv 1); by (asm_simp_tac (simpset() addsimps [diff_add_inverse]) 1); by (simp_tac (simpset() addsimps [le_add1]) 1); by (Asm_simp_tac 1); qed_spec_mp "gen_t_le_gen_alpha_t"; Addsimps [gen_t_le_gen_alpha_t];