# HG changeset patch # User wenzelm # Date 966501268 -7200 # Node ID 3047ada4bc05300730851721c47003e68a148b0c # Parent 1adf6d761c97d3f134a4c7149b6af99bb780fe1f done; diff -r 1adf6d761c97 -r 3047ada4bc05 src/HOL/Lambda/T.thy --- a/src/HOL/Lambda/T.thy Thu Aug 17 10:34:11 2000 +0200 +++ b/src/HOL/Lambda/T.thy Thu Aug 17 10:34:28 2000 +0200 @@ -10,31 +10,37 @@ theory Type = InductTermi: -datatype type = +datatype "typ" = Atom nat - | Fun type type (infixr "=>" 200) + | Fun "typ" "typ" (infixr "=>" 200) consts - typing :: "((nat => type) * dB * type) set" + typing :: "((nat => typ) * dB * typ) set" syntax - "_typing" :: "[nat => type, dB, type] => bool" ("_ |- _ : _" [50,50,50] 50) - "_funs" :: "[type list, type] => type" (infixl "=>>" 150) + "_typing" :: "[nat => typ, dB, typ] => bool" ("_ |- _ : _" [50,50,50] 50) + "_funs" :: "[typ list, typ] => typ" (infixl "=>>" 150) translations "env |- t : T" == "(env, t, T) : typing" "Ts =>> T" == "foldr Fun Ts T" -declare IT.intros [intro!] (* FIXME *) +lemmas [intro!] = IT.BetaI IT.LambdaI IT.VarI + +(* FIXME +declare IT.intros [intro!] +*) inductive typing -intros [intro!] +intros (* FIXME [intro!] *) Var: "env x = T ==> env |- Var x : T" Abs: "(nat_case T env) |- t : U ==> env |- (Abs t) : (T => U)" App: "env |- s : T => U ==> env |- t : T ==> env |- (s $ t) : U" +lemmas [intro!] = App Abs Var + consts - "types" :: "[nat => type, dB list, type list] => bool" + "types" :: "[nat => typ, dB list, typ list] => bool" primrec "types e [] Ts = (Ts = [])" "types e (t # ts) Ts = @@ -42,12 +48,13 @@ [] => False | T # Ts => e |- t : T & types e ts Ts)" -inductive_cases [elim!] = - "e |- Var i : T" +(* FIXME order *) +inductive_cases [elim!]: + "e |- Abs t : T" "e |- t $ u : T" - "e |- Abs t : T" + "e |- Var i : T" -inductive_cases [elim!] = +inductive_cases [elim!]: "x # xs : lists S" @@ -79,7 +86,7 @@ apply (erule impE) apply assumption apply (elim exE conjE) - apply (mk_cases_tac "e |- t $ u : T") + apply (ind_cases "e |- t $ u : T") apply (rule_tac x = "Ta # Ts" in exI) apply simp done @@ -159,7 +166,7 @@ "ts : lists IT --> map (\t. lift t 0) ts : lists IT" apply (induct_tac ts) apply auto - done + done lemma shift_env [simp]: @@ -197,7 +204,7 @@ apply simp_all done -lemma lift_types: +lemma lift_types [rulify]: "\Ts. types e ts Ts --> types (\j. if j < i then e j else if j = i then U @@ -224,7 +231,7 @@ apply (intro strip) apply (case_tac "x = i") apply simp - apply (frule linorder_neq_iff [RS iffD1]) + apply (frule linorder_neq_iff [THEN iffD1]) apply (erule disjE) apply simp apply (rule typing.Var) @@ -266,16 +273,21 @@ apply blast apply blast apply (intro strip) - apply (mk_cases_tac "s $ t -> t'") - apply hyp_subst - apply (mk_cases_tac "env |- Abs t : T => U") + apply (ind_cases "s $ t -> t'") + apply hypsubst + apply (ind_cases "env |- Abs t : T => U") apply (rule subst_lemma) apply assumption prefer 2 apply assumption apply (rule ext) apply (case_tac j) - apply auto + + apply simp + apply simp + apply fast + apply fast + (* FIXME apply auto *) done text {* additional lemmas *} @@ -309,20 +321,17 @@ apply fast txt {* Beta *} apply (intro strip) - apply (simp (no_asm_use) add: subst_subst [RS sym]) + apply (simp (no_asm_use) add: subst_subst [symmetric]) apply (rule IT.BetaI) apply auto done lemma Var_IT: "Var n \ IT" -proof - - have "Var n $$ [] \ IT" - apply (rule IT.VarI) - apply (rule lists.Nil) - done - then show ?thesis by simp -qed - + apply (subgoal_tac "Var n $$ [] \ IT") + apply simp + apply (rule IT.VarI) + apply (rule lists.Nil) + done lemma app_Var_IT: "t : IT ==> t $ Var i : IT" apply (erule IT.induct) @@ -332,12 +341,12 @@ apply (rule lists.Cons) apply (rule Var_IT) apply (rule lists.Nil) - apply (rule IT.BetaI [where ?ss = "[]", unfold foldl_Nil [RS eq_reflection]]) + apply (rule IT.BetaI [where ?ss = "[]", unfold foldl_Nil [THEN eq_reflection]]) apply (erule subst_Var_IT) apply (rule Var_IT) apply (subst app_last) apply (rule IT.BetaI) - apply (subst app_last [RS sym]) + apply (subst app_last [symmetric]) apply assumption apply assumption done @@ -364,9 +373,9 @@ apply simp apply (drule list_app_typeD) apply (elim exE conjE) - apply (mk_cases_tac "e |- t $ u : T") - apply (mk_cases_tac "e |- Var i : T") - apply (drule_tac s = "(?T::type) => ?U" in sym) + apply (ind_cases "e |- t $ u : T") + apply (ind_cases "e |- Var i : T") + apply (drule_tac s = "(?T::typ) => ?U" in sym) apply simp apply (subgoal_tac "lift u 0 $ Var 0 : IT") prefer 2 @@ -376,7 +385,7 @@ apply (simp (no_asm_use)) apply (subgoal_tac "(Var 0 $$ map (%t. lift t 0) (map (%t. t[u/i]) list))[(u $ a[u/i])/0] : IT") - apply (simp (no_asm_use) del: map_compose add: map_compose [RS sym] o_def) + apply (simp (no_asm_use) del: map_compose add: map_compose [symmetric] o_def) apply (erule_tac x = "Ts =>> T" in allE) apply (erule impE) apply simp @@ -387,86 +396,89 @@ apply (rule lifts_IT) apply (drule lists_types) apply - (mk_cases_tac "x # xs : lists (Collect P)", - erule lists_IntI [RS lists.induct], + (ind_cases "x # xs : lists (Collect P)", + erule lists_IntI [THEN lists.induct], assumption) apply fastsimp apply fastsimp - apply (erule_tac x = e in allE) - apply (erule_tac x = T in allE) - apply (erule_tac x = "u $ a[u/i]" in allE) - apply (erule_tac x = 0 in allE) - apply (force intro!: lift_types list_app_typeI substs_lemma subst_lemma) + apply (erule_tac x = e in allE) + apply (erule_tac x = T in allE) + apply (erule_tac x = "u $ a[u/i]" in allE) + apply (erule_tac x = 0 in allE) + apply (fastsimp intro!: list_app_typeI lift_types subst_lemma substs_lemma) + +(* FIXME + apply (tactic { * fast_tac (claset() + addSIs [thm "list_app_typeI", thm "lift_types", thm "subst_lemma", thm "substs_lemma"] + addss simpset()) 1 * }) *) -by (eres_inst_tac [("x", "Ta")] allE 1); -by (etac impE 1); -by (Simp_tac 1); -by (eres_inst_tac [("x", "lift u 0 $ Var 0")] allE 1); -by (etac impE 1); -by (assume_tac 1); -by (eres_inst_tac [("x", "e")] allE 1); -by (eres_inst_tac [("x", "Ts =>> T")] allE 1); -by (eres_inst_tac [("x", "a[u/i]")] allE 1); -by (eres_inst_tac [("x", "0")] allE 1); -by (etac impE 1); -by (rtac typing.APP 1); -by (etac lift_type' 1); -by (rtac typing.VAR 1); -by (Simp_tac 1); -by (fast_tac (claset() addSIs [subst_lemma]) 1); -(** n~=i **) -by (dtac list_app_typeD 1); -by (etac exE 1); -by (etac conjE 1); -by (dtac lists_types 1); -by (subgoal_tac "map (%x. x[u/i]) rs : lists IT" 1); -by (asm_simp_tac (simpset() addsimps [subst_Var]) 1); -by (Fast_tac 1); -by (etac (lists_IntI RS lists.induct) 1); -by (assume_tac 1); -by (fast_tac (claset() addss simpset()) 1); -by (fast_tac (claset() addss simpset()) 1); -(** Lambda **) -by (fast_tac (claset() addss simpset()) 1); -(** Beta **) -by (strip_tac 1); -by (Simp_tac 1); -by (rtac IT.BetaI 1); -by (simp_tac (simpset() delsimps [subst_map] - addsimps [subst_subst, subst_map RS sym]) 1); -by (dtac subject_reduction 1); -by (rtac apps_preserves_beta 1); -by (rtac beta.beta 1); -by (Fast_tac 1); -by (dtac list_app_typeD 1); -by (Fast_tac 1); -qed_spec_mp "subst_type_IT"; - -done + apply (erule_tac x = Ta in allE) + apply (erule impE) + apply simp + apply (erule_tac x = "lift u 0 $ Var 0" in allE) + apply (erule impE) + apply assumption + apply (erule_tac x = e in allE) + apply (erule_tac x = "Ts =>> T" in allE) + apply (erule_tac x = "a[u/i]" in allE) + apply (erule_tac x = 0 in allE) + apply (erule impE) + apply (rule typing.App) + apply (erule lift_type') + apply (rule typing.Var) + apply simp + apply (fast intro!: subst_lemma) + txt {* n~=i *} + apply (drule list_app_typeD) + apply (erule exE) + apply (erule conjE) + apply (drule lists_types) + apply (subgoal_tac "map (%x. x[u/i]) rs : lists IT") + apply (simp add: subst_Var) + apply fast + apply (erule lists_IntI [THEN lists.induct]) + apply assumption + apply fastsimp + apply fastsimp + txt {* Lambda *} + apply fastsimp + txt {* Beta *} + apply (intro strip) + apply (simp (no_asm)) + apply (rule IT.BetaI) + apply (simp (no_asm) del: subst_map add: subst_subst subst_map [symmetric]) + apply (drule subject_reduction) + apply (rule apps_preserves_beta) + apply (rule beta.beta) + apply fast + apply (drule list_app_typeD) + apply fast + done - - - -(**** main theorem: well-typed terms are strongly normalizing ****) +text {* main theorem: well-typed terms are strongly normalizing *} -Goal "e |- t : T ==> t : IT"; -by (etac typing.induct 1); -by (rtac Var_IT 1); -by (etac IT.LambdaI 1); -by (subgoal_tac "(Var 0 $ lift t 0)[s/0] : IT" 1); -by (Asm_full_simp_tac 1); -by (rtac subst_type_IT 1); -by (rtac (rewrite_rule (map mk_meta_eq [foldl_Nil, foldl_Cons]) - (lists.Nil RSN (2, lists.Cons RS IT.VarI))) 1); -by (etac lift_IT 1); -by (rtac typing.APP 1); -by (rtac typing.VAR 1); -by (Simp_tac 1); -by (etac lift_type' 1); -by (assume_tac 1); -by (assume_tac 1); -qed "type_implies_IT"; +lemma type_implies_IT: "e |- t : T ==> t : IT" + apply (erule typing.induct) + apply (rule Var_IT) + apply (erule IT.LambdaI) + apply (subgoal_tac "(Var 0 $ lift t 0)[s/0] : IT") + apply simp + apply (rule subst_type_IT) + apply (rule lists.Nil [THEN 2 lists.Cons [THEN IT.VarI], unfold foldl_Nil [THEN eq_reflection] + foldl_Cons [THEN eq_reflection]]) + apply (erule lift_IT) + apply (rule typing.App) + apply (rule typing.Var) + apply simp + apply (erule lift_type') + apply assumption + apply assumption + done -bind_thm ("type_implies_termi", type_implies_IT RS IT_implies_termi); +theorem type_implies_termi: "e |- t : T ==> t : termi beta" + apply (rule IT_implies_termi) + apply (erule type_implies_IT) + done +end