(* generated by Ott 0.10.14 from: caml_typedef_syntax.ott caml_typedef_typing.ott caml_typedef_reduction.ott *) (* to compile: Holmake caml_typedefTheory.uo *) (* for interactive use: app load ["pred_setTheory","finite_mapTheory","stringTheory","containerTheory","ottLib"]; *) open HolKernel boolLib Parse bossLib ottLib; infix THEN THENC |-> ## ; local open arithmeticTheory stringTheory containerTheory pred_setTheory listTheory finite_mapTheory in end; val _ = new_theory "caml_typedef"; local open integerTheory sortingTheory floatTheory integer_wordTheory in end; val _ = wordsLib.mk_word_size 31; (** syntax *) val _ = type_abbrev("index", ``:num``); val _ = type_abbrev("ident", ``:string``); val _ = type_abbrev("integer_literal", ``:word31``); val _ = type_abbrev("float_literal", ``:float``); val _ = type_abbrev("char_literal", ``:char``); val _ = type_abbrev("string_literal", ``:string``); val _ = type_abbrev("infix_symbol", ``:string``); val _ = type_abbrev("prefix_symbol", ``:string``); val _ = type_abbrev("location", ``:num``); val _ = type_abbrev("lowercase_ident", ``:string``); val _ = type_abbrev("capitalized_ident", ``:string``); val _ = Hol_datatype ` typeconstr_name = TCN_id of lowercase_ident `; val _ = Hol_datatype ` typeconstr = TC_name of typeconstr_name | TC_int | TC_char | TC_string | TC_float | TC_bool | TC_unit | TC_exn | TC_list | TC_option | TC_ref `; val _ = type_abbrev("idx", ``:num``); val _ = Hol_datatype ` typevar = TV_ident of ident `; val _ = Hol_datatype ` constr_name = CN_id of capitalized_ident `; val _ = Hol_datatype ` typexpr = TE_var of typevar | TE_idxvar of idx => idx | TE_any | TE_arrow of typexpr => typexpr | TE_tuple of typexpr list | TE_constr of typexpr list => typeconstr `; val _ = Hol_datatype ` field_name = FN_id of lowercase_ident `; val _ = Hol_datatype ` infix_op = IO_symbol of infix_symbol | IO_star | IO_equal | IO_colonequal `; val _ = Hol_datatype ` constr_decl = CD_nullary of constr_name | CD_nary of constr_name => typexpr list `; val _ = Hol_datatype ` field_decl = FD_immutable of field_name => typexpr `; val _ = Hol_datatype ` operator_name = ON_symbol of prefix_symbol | ON_infix of infix_op `; val _ = Hol_datatype ` constr = C_name of constr_name | C_invalidargument | C_notfound | C_assertfailure | C_matchfailure | C_div_by_0 | C_none | C_some `; val _ = type_abbrev("intn", ``:word31``); val _ = Hol_datatype ` type_equation = TE_te of typexpr `; val _ = Hol_datatype ` type_representation = TR_variant of constr_decl list | TR_record of field_decl list `; val _ = Hol_datatype ` type_param = TP_var of typevar `; val _ = Hol_datatype ` value_name = VN_id of lowercase_ident | VN_op of operator_name `; val _ = Hol_datatype ` field = F_name of field_name `; val _ = Hol_datatype ` constant = CONST_int of intn | CONST_float of float_literal | CONST_char of char_literal | CONST_string of string_literal | CONST_constr of constr | CONST_false | CONST_true | CONST_nil | CONST_unit `; val _ = Hol_datatype ` type_information = TI_eq of type_equation | TI_def of type_representation `; val _ = Hol_datatype ` type_params_opt = TPS_nary of type_param list `; val _ = Hol_datatype ` pattern = P_var of value_name | P_any | P_constant of constant | P_alias of pattern => value_name | P_typed of pattern => typexpr | P_or of pattern => pattern | P_construct of constr => pattern list | P_construct_any of constr | P_tuple of pattern list | P_record of (field#pattern) list | P_cons of pattern => pattern `; val _ = Hol_datatype ` unary_prim = Uprim_raise | Uprim_not | Uprim_minus | Uprim_ref | Uprim_deref `; val _ = Hol_datatype ` binary_prim = Bprim_equal | Bprim_plus | Bprim_minus | Bprim_times | Bprim_div | Bprim_assign `; val _ = Hol_datatype ` for_dirn = FD_upto | FD_downto `; val _ = Hol_datatype ` typedef = TD_td of type_params_opt => typeconstr_name => type_information `; val _ = Hol_datatype ` letrec_binding = LRB_simple of value_name => pattern_matching ; letrec_bindings = LRBs_inj of letrec_binding list ; let_binding = LB_simple of pattern => expr ; pat_exp = PE_inj of pattern => expr ; pattern_matching = PM_pm of pat_exp list ; expr = Expr_uprim of unary_prim | Expr_bprim of binary_prim | Expr_ident of value_name | Expr_constant of constant | Expr_typed of expr => typexpr | Expr_tuple of expr list | Expr_construct of constr => expr list | Expr_cons of expr => expr | Expr_record of (field#expr) list | Expr_override of expr => (field#expr) list | Expr_apply of expr => expr | Expr_and of expr => expr | Expr_or of expr => expr | Expr_field of expr => field | Expr_ifthenelse of expr => expr => expr | Expr_while of expr => expr | Expr_for of value_name => expr => for_dirn => expr => expr | Expr_sequence of expr => expr | Expr_match of expr => pattern_matching | Expr_function of pattern_matching | Expr_try of expr => pattern_matching | Expr_let of let_binding => expr | Expr_letrec of letrec_bindings => expr | Expr_assert of expr | Expr_location of location `; val _ = Hol_datatype ` type_definition = TDF_tdf of typedef list `; val _ = Hol_datatype ` exception_definition = ED_def of constr_decl `; val _ = Hol_datatype ` definition = D_let of let_binding | D_letrec of letrec_bindings | D_type of type_definition | D_exception of exception_definition `; val _ = Hol_datatype ` typescheme = TS_forall of typexpr `; val _ = type_abbrev("kind", ``:num``); val _ = Hol_datatype ` typexprs = typexprs_inj of typexpr list `; val _ = Hol_datatype ` trans_label = Lab_nil | Lab_alloc of expr => location | Lab_deref of location => expr | Lab_assign of location => expr `; val _ = Hol_datatype ` definitions = Ds_nil | Ds_cons of definition => definitions `; val _ = Hol_datatype ` name = name_tv | name_vn of value_name | name_cn of constr_name | name_tcn of typeconstr_name | name_fn of field_name | name_l of location `; val _ = Hol_datatype ` environment_binding = EB_tv | EB_vn of value_name => typescheme | EB_cc of constr_name => typeconstr | EB_pc of constr_name => type_params_opt => typexprs => typeconstr | EB_fn of field_name => type_params_opt => typeconstr_name => typexpr | EB_td of typeconstr_name => kind | EB_tr of typeconstr_name => kind => field_name list | EB_ta of type_params_opt => typeconstr_name => typexpr | EB_l of location => typexpr `; val _ = type_abbrev("labelled_arrow", ``:trans_label``); val _ = Hol_datatype ` program = Prog_defs of definitions | Prog_raise of expr `; val _ = type_abbrev("store", ``:((location#expr) list)``); val _ = type_abbrev("names", ``:(name list)``); val _ = type_abbrev("environment", ``:(environment_binding list)``); val _ = type_abbrev("Tsigma", ``:(typevar#typexpr) list``); val _ = Hol_datatype ` substs_x = substs_x_xs of (value_name#expr) list `; val _ = Hol_datatype ` value_path = VP_name of value_name `; (** subrules *) val _ = ottDefine "is_binary_prim_app_value_of_expr" ` ( is_binary_prim_app_value_of_expr (Expr_uprim unary_prim) = F) /\ ( is_binary_prim_app_value_of_expr (Expr_bprim binary_prim) = (T)) /\ ( is_binary_prim_app_value_of_expr (Expr_ident value_name) = F) /\ ( is_binary_prim_app_value_of_expr (Expr_constant constant) = F) /\ ( is_binary_prim_app_value_of_expr (Expr_typed expr typexpr) = F) /\ ( is_binary_prim_app_value_of_expr (Expr_tuple (expr_list)) = F) /\ ( is_binary_prim_app_value_of_expr (Expr_construct constr (expr_list)) = F) /\ ( is_binary_prim_app_value_of_expr (Expr_cons expr1 expr2) = F) /\ ( is_binary_prim_app_value_of_expr (Expr_record (field_expr_list)) = F) /\ ( is_binary_prim_app_value_of_expr (Expr_override expr (field_expr_list)) = F) /\ ( is_binary_prim_app_value_of_expr (Expr_apply expr1 expr2) = F) /\ ( is_binary_prim_app_value_of_expr (Expr_and expr1 expr2) = F) /\ ( is_binary_prim_app_value_of_expr (Expr_or expr1 expr2) = F) /\ ( is_binary_prim_app_value_of_expr (Expr_field expr field) = F) /\ ( is_binary_prim_app_value_of_expr (Expr_ifthenelse expr0 expr1 expr2) = F) /\ ( is_binary_prim_app_value_of_expr (Expr_while expr1 expr2) = F) /\ ( is_binary_prim_app_value_of_expr (Expr_for x expr1 for_dirn expr2 expr3) = F) /\ ( is_binary_prim_app_value_of_expr (Expr_sequence expr1 expr2) = F) /\ ( is_binary_prim_app_value_of_expr (Expr_match expr pattern_matching) = F) /\ ( is_binary_prim_app_value_of_expr (Expr_function pattern_matching) = F) /\ ( is_binary_prim_app_value_of_expr (Expr_try expr pattern_matching) = F) /\ ( is_binary_prim_app_value_of_expr (Expr_let let_binding expr) = F) /\ ( is_binary_prim_app_value_of_expr (Expr_letrec letrec_bindings expr) = F) /\ ( is_binary_prim_app_value_of_expr (Expr_assert expr) = F) /\ ( is_binary_prim_app_value_of_expr (Expr_location location) = F) `; val _ = ottDefine "is_definition_value_of_definition" ` ( is_definition_value_of_definition (D_let let_binding) = F) /\ ( is_definition_value_of_definition (D_letrec letrec_bindings) = F) /\ ( is_definition_value_of_definition (D_type type_definition) = (T)) /\ ( is_definition_value_of_definition (D_exception exception_definition) = (T)) `; val _ = ottDefine "is_value_of_expr" ` ( is_value_of_expr (Expr_uprim unary_prim) = (T)) /\ ( is_value_of_expr (Expr_bprim binary_prim) = (T)) /\ ( is_value_of_expr (Expr_ident value_name) = F) /\ ( is_value_of_expr (Expr_constant constant) = (T)) /\ ( is_value_of_expr (Expr_typed expr typexpr) = F) /\ ( is_value_of_expr (Expr_tuple (expr_list)) = ((EVERY (\expr_. (is_value_of_expr expr_)) expr_list))) /\ ( is_value_of_expr (Expr_construct constr (expr_list)) = ((EVERY (\expr_. (is_value_of_expr expr_)) expr_list))) /\ ( is_value_of_expr (Expr_cons expr1 expr2) = ((is_value_of_expr expr1) /\ (is_value_of_expr expr2))) /\ ( is_value_of_expr (Expr_record (field_expr_list)) = ((EVERY (\(field_,expr_). (is_value_of_expr expr_)) field_expr_list))) /\ ( is_value_of_expr (Expr_override expr (field_expr_list)) = F) /\ ( is_value_of_expr (Expr_apply expr1 expr2) = ((is_binary_prim_app_value_of_expr expr1) /\ (is_value_of_expr expr2))) /\ ( is_value_of_expr (Expr_and expr1 expr2) = F) /\ ( is_value_of_expr (Expr_or expr1 expr2) = F) /\ ( is_value_of_expr (Expr_field expr field) = F) /\ ( is_value_of_expr (Expr_ifthenelse expr0 expr1 expr2) = F) /\ ( is_value_of_expr (Expr_while expr1 expr2) = F) /\ ( is_value_of_expr (Expr_for x expr1 for_dirn expr2 expr3) = F) /\ ( is_value_of_expr (Expr_sequence expr1 expr2) = F) /\ ( is_value_of_expr (Expr_match expr pattern_matching) = F) /\ ( is_value_of_expr (Expr_function pattern_matching) = (T)) /\ ( is_value_of_expr (Expr_try expr pattern_matching) = F) /\ ( is_value_of_expr (Expr_let let_binding expr) = F) /\ ( is_value_of_expr (Expr_letrec letrec_bindings expr) = F) /\ ( is_value_of_expr (Expr_assert expr) = F) /\ ( is_value_of_expr (Expr_location location) = (T)) `; val _ = ottDefine "is_non_expansive_of_expr" ` ( is_non_expansive_of_expr (Expr_uprim unary_prim) = (T)) /\ ( is_non_expansive_of_expr (Expr_bprim binary_prim) = (T)) /\ ( is_non_expansive_of_expr (Expr_ident value_name) = (T)) /\ ( is_non_expansive_of_expr (Expr_constant constant) = (T)) /\ ( is_non_expansive_of_expr (Expr_typed expr typexpr) = ((is_non_expansive_of_expr expr))) /\ ( is_non_expansive_of_expr (Expr_tuple (expr_list)) = ((EVERY (\expr_. (is_non_expansive_of_expr expr_)) expr_list))) /\ ( is_non_expansive_of_expr (Expr_construct constr (expr_list)) = ((EVERY (\expr_. (is_non_expansive_of_expr expr_)) expr_list))) /\ ( is_non_expansive_of_expr (Expr_cons expr1 expr2) = ((is_non_expansive_of_expr expr1) /\ (is_non_expansive_of_expr expr2))) /\ ( is_non_expansive_of_expr (Expr_record (field_expr_list)) = ((EVERY (\(field_,expr_). (is_non_expansive_of_expr expr_)) field_expr_list))) /\ ( is_non_expansive_of_expr (Expr_override expr (field_expr_list)) = F) /\ ( is_non_expansive_of_expr (Expr_apply expr1 expr2) = ((is_binary_prim_app_value_of_expr expr1) /\ (is_non_expansive_of_expr expr2))) /\ ( is_non_expansive_of_expr (Expr_and expr1 expr2) = F) /\ ( is_non_expansive_of_expr (Expr_or expr1 expr2) = F) /\ ( is_non_expansive_of_expr (Expr_field expr field) = F) /\ ( is_non_expansive_of_expr (Expr_ifthenelse expr0 expr1 expr2) = F) /\ ( is_non_expansive_of_expr (Expr_while expr1 expr2) = F) /\ ( is_non_expansive_of_expr (Expr_for x expr1 for_dirn expr2 expr3) = F) /\ ( is_non_expansive_of_expr (Expr_sequence expr1 expr2) = F) /\ ( is_non_expansive_of_expr (Expr_match expr pattern_matching) = F) /\ ( is_non_expansive_of_expr (Expr_function pattern_matching) = (T)) /\ ( is_non_expansive_of_expr (Expr_try expr pattern_matching) = F) /\ ( is_non_expansive_of_expr (Expr_let let_binding expr) = F) /\ ( is_non_expansive_of_expr (Expr_letrec letrec_bindings expr) = ((is_non_expansive_of_expr expr))) /\ ( is_non_expansive_of_expr (Expr_assert expr) = F) /\ ( is_non_expansive_of_expr (Expr_location location) = (T)) `; val _ = ottDefine "is_src_typexpr_of_typexpr" ` ( is_src_typexpr_of_typexpr (TE_var typevar) = (T)) /\ ( is_src_typexpr_of_typexpr (TE_idxvar idx num) = F) /\ ( is_src_typexpr_of_typexpr TE_any = (T)) /\ ( is_src_typexpr_of_typexpr (TE_arrow typexpr1 typexpr2) = ((is_src_typexpr_of_typexpr typexpr1) /\ (is_src_typexpr_of_typexpr typexpr2))) /\ ( is_src_typexpr_of_typexpr (TE_tuple (typexpr_list)) = ((EVERY (\typexpr_. (is_src_typexpr_of_typexpr typexpr_)) typexpr_list))) /\ ( is_src_typexpr_of_typexpr (TE_constr (typexpr_list) typeconstr) = ((EVERY (\typexpr_. (is_src_typexpr_of_typexpr typexpr_)) typexpr_list))) `; val _ = ottDefine "is_definitions_value_of_definitions" ` ( is_definitions_value_of_definitions Ds_nil = (T)) /\ ( is_definitions_value_of_definitions (Ds_cons definition definitions) = ((is_definition_value_of_definition definition) /\ (is_definitions_value_of_definitions definitions))) `; val _ = ottDefine "is_trans_label_of_trans_label" ` ( is_trans_label_of_trans_label Lab_nil = (T)) /\ ( is_trans_label_of_trans_label (Lab_alloc v location) = ((is_value_of_expr v))) /\ ( is_trans_label_of_trans_label (Lab_deref location v) = ((is_value_of_expr v))) /\ ( is_trans_label_of_trans_label (Lab_assign location v) = ((is_value_of_expr v))) `; (** auxiliary functions *) val _ = ottDefine "aux_constr_names_constr_decl_of_constr_decl" ` ( aux_constr_names_constr_decl_of_constr_decl (CD_nullary constr_name) = [constr_name]) /\ ( aux_constr_names_constr_decl_of_constr_decl (CD_nary constr_name (typexpr_list)) = [constr_name]) `; val _ = ottDefine "aux_constr_names_type_representation_of_type_representation" ` ( aux_constr_names_type_representation_of_type_representation (TR_variant (constr_decl_list)) = (FLAT (MAP aux_constr_names_constr_decl_of_constr_decl (constr_decl_list)))) /\ ( aux_constr_names_type_representation_of_type_representation (TR_record (field_decl_list)) = []) `; val _ = ottDefine "aux_constr_names_type_information_of_type_information" ` ( aux_constr_names_type_information_of_type_information (TI_eq type_equation) = []) /\ ( aux_constr_names_type_information_of_type_information (TI_def type_representation) = (aux_constr_names_type_representation_of_type_representation type_representation)) `; val _ = ottDefine "aux_field_names_field_decl_of_field_decl" ` ( aux_field_names_field_decl_of_field_decl (FD_immutable field_name typexpr) = [field_name]) `; val _ = ottDefine "aux_xs_pattern_of_pattern" ` ( aux_xs_pattern_of_pattern (P_var value_name) = [value_name]) /\ ( aux_xs_pattern_of_pattern P_any = []) /\ ( aux_xs_pattern_of_pattern (P_constant constant) = []) /\ ( aux_xs_pattern_of_pattern (P_alias pattern value_name) = ((aux_xs_pattern_of_pattern pattern) ++ [value_name])) /\ ( aux_xs_pattern_of_pattern (P_typed pattern typexpr) = (aux_xs_pattern_of_pattern pattern)) /\ ( aux_xs_pattern_of_pattern (P_or pattern1 pattern2) = (aux_xs_pattern_of_pattern pattern1)) /\ ( aux_xs_pattern_of_pattern (P_construct constr (pattern_list)) = (FLAT (MAP aux_xs_pattern_of_pattern (pattern_list)))) /\ ( aux_xs_pattern_of_pattern (P_construct_any constr) = []) /\ ( aux_xs_pattern_of_pattern (P_tuple (pattern_list)) = (FLAT (MAP aux_xs_pattern_of_pattern (pattern_list)))) /\ ( aux_xs_pattern_of_pattern (P_record (field_pattern_list)) = (FLAT (MAP aux_xs_pattern_of_pattern ((MAP (\(field_,pattern_) . pattern_) field_pattern_list))))) /\ ( aux_xs_pattern_of_pattern (P_cons pattern1 pattern2) = ((aux_xs_pattern_of_pattern pattern1) ++ (aux_xs_pattern_of_pattern pattern2))) `; val _ = ottDefine "aux_xs_letrec_binding_of_letrec_binding" ` ( aux_xs_letrec_binding_of_letrec_binding (LRB_simple value_name pattern_matching) = [value_name]) `; val _ = ottDefine "aux_constr_names_typedef_of_typedef" ` ( aux_constr_names_typedef_of_typedef (TD_td type_params_opt typeconstr_name type_information) = (aux_constr_names_type_information_of_type_information type_information)) `; val _ = ottDefine "aux_field_names_type_representation_of_type_representation" ` ( aux_field_names_type_representation_of_type_representation (TR_variant (constr_decl_list)) = []) /\ ( aux_field_names_type_representation_of_type_representation (TR_record (field_decl_list)) = (FLAT (MAP aux_field_names_field_decl_of_field_decl (field_decl_list)))) `; val _ = ottDefine "aux_type_names_typedef_of_typedef" ` ( aux_type_names_typedef_of_typedef (TD_td type_params_opt typeconstr_name type_information) = [typeconstr_name]) `; val _ = ottDefine "aux_typevars_type_param_of_type_param" ` ( aux_typevars_type_param_of_type_param (TP_var typevar) = [typevar]) `; val _ = ottDefine "aux_xs_let_binding_of_let_binding" ` ( aux_xs_let_binding_of_let_binding (LB_simple pattern expr) = (aux_xs_pattern_of_pattern pattern)) `; val _ = ottDefine "aux_xs_letrec_bindings_of_letrec_bindings" ` ( aux_xs_letrec_bindings_of_letrec_bindings (LRBs_inj (letrec_binding_list)) = (FLAT (MAP aux_xs_letrec_binding_of_letrec_binding (letrec_binding_list)))) `; val _ = ottDefine "aux_constr_names_type_definition_of_type_definition" ` ( aux_constr_names_type_definition_of_type_definition (TDF_tdf (typedef_list)) = (FLAT (MAP aux_constr_names_typedef_of_typedef (typedef_list)))) `; val _ = ottDefine "aux_field_names_type_information_of_type_information" ` ( aux_field_names_type_information_of_type_information (TI_eq type_equation) = []) /\ ( aux_field_names_type_information_of_type_information (TI_def type_representation) = (aux_field_names_type_representation_of_type_representation type_representation)) `; val _ = ottDefine "aux_type_names_type_definition_of_type_definition" ` ( aux_type_names_type_definition_of_type_definition (TDF_tdf (typedef_list)) = (FLAT (MAP aux_type_names_typedef_of_typedef (typedef_list)))) `; val _ = ottDefine "aux_typevars_type_params_opt_of_type_params_opt" ` ( aux_typevars_type_params_opt_of_type_params_opt (TPS_nary (type_param_list)) = (FLAT (MAP aux_typevars_type_param_of_type_param (type_param_list)))) `; val _ = ottDefine "aux_xs_definition_of_definition" ` ( aux_xs_definition_of_definition (D_let let_binding) = (aux_xs_let_binding_of_let_binding let_binding)) /\ ( aux_xs_definition_of_definition (D_letrec letrec_bindings) = (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings)) /\ ( aux_xs_definition_of_definition (D_type type_definition) = []) /\ ( aux_xs_definition_of_definition (D_exception exception_definition) = []) `; (** free variables *) val _ = ottDefine "ftv_typexpr" ` ( ftv_typexpr (TE_var typevar) = [typevar]) /\ ( ftv_typexpr (TE_idxvar idx num) = []) /\ ( ftv_typexpr TE_any = []) /\ ( ftv_typexpr (TE_arrow typexpr1 typexpr2) = (ftv_typexpr typexpr1) ++ (ftv_typexpr typexpr2)) /\ ( ftv_typexpr (TE_tuple (typexpr_list)) = (FLAT (MAP (\typexpr_. (ftv_typexpr typexpr_)) typexpr_list))) /\ ( ftv_typexpr (TE_constr (typexpr_list) typeconstr) = (FLAT (MAP (\typexpr_. (ftv_typexpr typexpr_)) typexpr_list))) `; val _ = ottDefine "ftv_constr_decl" ` ( ftv_constr_decl (CD_nullary constr_name) = []) /\ ( ftv_constr_decl (CD_nary constr_name (typexpr_list)) = (FLAT (MAP (\typexpr_. (ftv_typexpr typexpr_)) typexpr_list))) `; val _ = ottDefine "ftv_field_decl" ` ( ftv_field_decl (FD_immutable field_name typexpr) = (ftv_typexpr typexpr)) `; val _ = ottDefine "ftv_type_equation" ` ( ftv_type_equation (TE_te typexpr) = (ftv_typexpr typexpr)) `; val _ = ottDefine "ftv_type_representation" ` ( ftv_type_representation (TR_variant (constr_decl_list)) = (FLAT (MAP (\constr_decl_. (ftv_constr_decl constr_decl_)) constr_decl_list))) /\ ( ftv_type_representation (TR_record (field_decl_list)) = (FLAT (MAP (\field_decl_. (ftv_field_decl field_decl_)) field_decl_list))) `; val _ = ottDefine "ftv_type_information" ` ( ftv_type_information (TI_eq type_equation) = (ftv_type_equation type_equation)) /\ ( ftv_type_information (TI_def type_representation) = (ftv_type_representation type_representation)) `; val _ = ottDefine "ftv_pattern" ` ( ftv_pattern (P_var value_name) = []) /\ ( ftv_pattern P_any = []) /\ ( ftv_pattern (P_constant constant) = []) /\ ( ftv_pattern (P_alias pattern value_name) = (ftv_pattern pattern)) /\ ( ftv_pattern (P_typed pattern typexpr) = (ftv_pattern pattern) ++ (ftv_typexpr typexpr)) /\ ( ftv_pattern (P_or pattern1 pattern2) = (ftv_pattern pattern1) ++ (ftv_pattern pattern2)) /\ ( ftv_pattern (P_construct constr (pattern_list)) = (FLAT (MAP (\pattern_. (ftv_pattern pattern_)) pattern_list))) /\ ( ftv_pattern (P_construct_any constr) = []) /\ ( ftv_pattern (P_tuple (pattern_list)) = (FLAT (MAP (\pattern_. (ftv_pattern pattern_)) pattern_list))) /\ ( ftv_pattern (P_record (field_pattern_list)) = (FLAT (MAP (\(field_,pattern_). (ftv_pattern pattern_)) field_pattern_list))) /\ ( ftv_pattern (P_cons pattern1 pattern2) = (ftv_pattern pattern1) ++ (ftv_pattern pattern2)) `; val _ = ottDefine "ftv_typedef" ` ( ftv_typedef (TD_td type_params_opt typeconstr_name type_information) = (list_minus (ftv_type_information type_information) (aux_typevars_type_params_opt_of_type_params_opt type_params_opt))) `; val _ = ottDefine "ftv_letrec_binding" ` ( ftv_letrec_binding (LRB_simple value_name pattern_matching) = (ftv_pattern_matching pattern_matching)) /\ ( ftv_letrec_bindings (LRBs_inj (letrec_binding_list)) = (FLAT (MAP (\letrec_binding_. (ftv_letrec_binding letrec_binding_)) letrec_binding_list))) /\ ( ftv_let_binding (LB_simple pattern expr) = (ftv_pattern pattern) ++ (ftv_expr expr)) /\ ( ftv_pat_exp (PE_inj pattern expr) = (ftv_pattern pattern) ++ (ftv_expr expr)) /\ ( ftv_pattern_matching (PM_pm (pat_exp_list)) = (FLAT (MAP (\pat_exp_. (ftv_pat_exp pat_exp_)) pat_exp_list))) /\ ( ftv_expr (Expr_uprim unary_prim) = []) /\ ( ftv_expr (Expr_bprim binary_prim) = []) /\ ( ftv_expr (Expr_ident value_name) = []) /\ ( ftv_expr (Expr_constant constant) = []) /\ ( ftv_expr (Expr_typed expr typexpr) = (ftv_expr expr) ++ (ftv_typexpr typexpr)) /\ ( ftv_expr (Expr_tuple (expr_list)) = (FLAT (MAP (\expr_. (ftv_expr expr_)) expr_list))) /\ ( ftv_expr (Expr_construct constr (expr_list)) = (FLAT (MAP (\expr_. (ftv_expr expr_)) expr_list))) /\ ( ftv_expr (Expr_cons expr1 expr2) = (ftv_expr expr1) ++ (ftv_expr expr2)) /\ ( ftv_expr (Expr_record (field_expr_list)) = (FLAT (MAP (\(field_,expr_). (ftv_expr expr_)) field_expr_list))) /\ ( ftv_expr (Expr_override expr (field_expr_list)) = (ftv_expr expr) ++ (FLAT (MAP (\(field_,expr_). (ftv_expr expr_)) field_expr_list))) /\ ( ftv_expr (Expr_apply expr1 expr2) = (ftv_expr expr1) ++ (ftv_expr expr2)) /\ ( ftv_expr (Expr_and expr1 expr2) = (ftv_expr expr1) ++ (ftv_expr expr2)) /\ ( ftv_expr (Expr_or expr1 expr2) = (ftv_expr expr1) ++ (ftv_expr expr2)) /\ ( ftv_expr (Expr_field expr field) = (ftv_expr expr)) /\ ( ftv_expr (Expr_ifthenelse expr0 expr1 expr2) = (ftv_expr expr0) ++ (ftv_expr expr1) ++ (ftv_expr expr2)) /\ ( ftv_expr (Expr_while expr1 expr2) = (ftv_expr expr1) ++ (ftv_expr expr2)) /\ ( ftv_expr (Expr_for x expr1 for_dirn expr2 expr3) = (ftv_expr expr1) ++ (ftv_expr expr2) ++ (ftv_expr expr3)) /\ ( ftv_expr (Expr_sequence expr1 expr2) = (ftv_expr expr1) ++ (ftv_expr expr2)) /\ ( ftv_expr (Expr_match expr pattern_matching) = (ftv_expr expr) ++ (ftv_pattern_matching pattern_matching)) /\ ( ftv_expr (Expr_function pattern_matching) = (ftv_pattern_matching pattern_matching)) /\ ( ftv_expr (Expr_try expr pattern_matching) = (ftv_expr expr) ++ (ftv_pattern_matching pattern_matching)) /\ ( ftv_expr (Expr_let let_binding expr) = (ftv_let_binding let_binding) ++ (ftv_expr expr)) /\ ( ftv_expr (Expr_letrec letrec_bindings expr) = (ftv_letrec_bindings letrec_bindings) ++ (ftv_expr expr)) /\ ( ftv_expr (Expr_assert expr) = (ftv_expr expr)) /\ ( ftv_expr (Expr_location location) = []) `; val _ = ottDefine "ftv_type_definition" ` ( ftv_type_definition (TDF_tdf (typedef_list)) = (FLAT (MAP (\typedef_. (ftv_typedef typedef_)) typedef_list))) `; val _ = ottDefine "ftv_exception_definition" ` ( ftv_exception_definition (ED_def constr_decl) = (ftv_constr_decl constr_decl)) `; val _ = ottDefine "fv_letrec_binding" ` ( fv_letrec_binding (LRB_simple value_name pattern_matching) = (fv_pattern_matching pattern_matching)) /\ ( fv_letrec_bindings (LRBs_inj (letrec_binding_list)) = (FLAT (MAP (\letrec_binding_. (fv_letrec_binding letrec_binding_)) letrec_binding_list))) /\ ( fv_let_binding (LB_simple pattern expr) = (fv_expr expr)) /\ ( fv_pat_exp (PE_inj pattern expr) = (list_minus (fv_expr expr) (aux_xs_pattern_of_pattern pattern))) /\ ( fv_pattern_matching (PM_pm (pat_exp_list)) = (FLAT (MAP (\pat_exp_. (fv_pat_exp pat_exp_)) pat_exp_list))) /\ ( fv_expr (Expr_uprim unary_prim) = []) /\ ( fv_expr (Expr_bprim binary_prim) = []) /\ ( fv_expr (Expr_ident value_name) = [value_name]) /\ ( fv_expr (Expr_constant constant) = []) /\ ( fv_expr (Expr_typed expr typexpr) = (fv_expr expr)) /\ ( fv_expr (Expr_tuple (expr_list)) = (FLAT (MAP (\expr_. (fv_expr expr_)) expr_list))) /\ ( fv_expr (Expr_construct constr (expr_list)) = (FLAT (MAP (\expr_. (fv_expr expr_)) expr_list))) /\ ( fv_expr (Expr_cons expr1 expr2) = (fv_expr expr1) ++ (fv_expr expr2)) /\ ( fv_expr (Expr_record (field_expr_list)) = (FLAT (MAP (\(field_,expr_). (fv_expr expr_)) field_expr_list))) /\ ( fv_expr (Expr_override expr (field_expr_list)) = (fv_expr expr) ++ (FLAT (MAP (\(field_,expr_). (fv_expr expr_)) field_expr_list))) /\ ( fv_expr (Expr_apply expr1 expr2) = (fv_expr expr1) ++ (fv_expr expr2)) /\ ( fv_expr (Expr_and expr1 expr2) = (fv_expr expr1) ++ (fv_expr expr2)) /\ ( fv_expr (Expr_or expr1 expr2) = (fv_expr expr1) ++ (fv_expr expr2)) /\ ( fv_expr (Expr_field expr field) = (fv_expr expr)) /\ ( fv_expr (Expr_ifthenelse expr0 expr1 expr2) = (fv_expr expr0) ++ (fv_expr expr1) ++ (fv_expr expr2)) /\ ( fv_expr (Expr_while expr1 expr2) = (fv_expr expr1) ++ (fv_expr expr2)) /\ ( fv_expr (Expr_for x expr1 for_dirn expr2 expr3) = (fv_expr expr1) ++ (fv_expr expr2) ++ (list_minus (fv_expr expr3) [x])) /\ ( fv_expr (Expr_sequence expr1 expr2) = (fv_expr expr1) ++ (fv_expr expr2)) /\ ( fv_expr (Expr_match expr pattern_matching) = (fv_expr expr) ++ (fv_pattern_matching pattern_matching)) /\ ( fv_expr (Expr_function pattern_matching) = (fv_pattern_matching pattern_matching)) /\ ( fv_expr (Expr_try expr pattern_matching) = (fv_expr expr) ++ (fv_pattern_matching pattern_matching)) /\ ( fv_expr (Expr_let let_binding expr) = (fv_let_binding let_binding) ++ (list_minus (fv_expr expr) (aux_xs_let_binding_of_let_binding let_binding))) /\ ( fv_expr (Expr_letrec letrec_bindings expr) = (list_minus (fv_letrec_bindings letrec_bindings) (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings)) ++ (list_minus (fv_expr expr) (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings))) /\ ( fv_expr (Expr_assert expr) = (fv_expr expr)) /\ ( fv_expr (Expr_location location) = []) `; val _ = ottDefine "fl_letrec_binding" ` ( fl_letrec_binding (LRB_simple value_name pattern_matching) = (fl_pattern_matching pattern_matching)) /\ ( fl_letrec_bindings (LRBs_inj (letrec_binding_list)) = (FLAT (MAP (\letrec_binding_. (fl_letrec_binding letrec_binding_)) letrec_binding_list))) /\ ( fl_let_binding (LB_simple pattern expr) = (fl_expr expr)) /\ ( fl_pat_exp (PE_inj pattern expr) = (fl_expr expr)) /\ ( fl_pattern_matching (PM_pm (pat_exp_list)) = (FLAT (MAP (\pat_exp_. (fl_pat_exp pat_exp_)) pat_exp_list))) /\ ( fl_expr (Expr_uprim unary_prim) = []) /\ ( fl_expr (Expr_bprim binary_prim) = []) /\ ( fl_expr (Expr_ident value_name) = []) /\ ( fl_expr (Expr_constant constant) = []) /\ ( fl_expr (Expr_typed expr typexpr) = (fl_expr expr)) /\ ( fl_expr (Expr_tuple (expr_list)) = (FLAT (MAP (\expr_. (fl_expr expr_)) expr_list))) /\ ( fl_expr (Expr_construct constr (expr_list)) = (FLAT (MAP (\expr_. (fl_expr expr_)) expr_list))) /\ ( fl_expr (Expr_cons expr1 expr2) = (fl_expr expr1) ++ (fl_expr expr2)) /\ ( fl_expr (Expr_record (field_expr_list)) = (FLAT (MAP (\(field_,expr_). (fl_expr expr_)) field_expr_list))) /\ ( fl_expr (Expr_override expr (field_expr_list)) = (fl_expr expr) ++ (FLAT (MAP (\(field_,expr_). (fl_expr expr_)) field_expr_list))) /\ ( fl_expr (Expr_apply expr1 expr2) = (fl_expr expr1) ++ (fl_expr expr2)) /\ ( fl_expr (Expr_and expr1 expr2) = (fl_expr expr1) ++ (fl_expr expr2)) /\ ( fl_expr (Expr_or expr1 expr2) = (fl_expr expr1) ++ (fl_expr expr2)) /\ ( fl_expr (Expr_field expr field) = (fl_expr expr)) /\ ( fl_expr (Expr_ifthenelse expr0 expr1 expr2) = (fl_expr expr0) ++ (fl_expr expr1) ++ (fl_expr expr2)) /\ ( fl_expr (Expr_while expr1 expr2) = (fl_expr expr1) ++ (fl_expr expr2)) /\ ( fl_expr (Expr_for x expr1 for_dirn expr2 expr3) = (fl_expr expr1) ++ (fl_expr expr2) ++ (fl_expr expr3)) /\ ( fl_expr (Expr_sequence expr1 expr2) = (fl_expr expr1) ++ (fl_expr expr2)) /\ ( fl_expr (Expr_match expr pattern_matching) = (fl_expr expr) ++ (fl_pattern_matching pattern_matching)) /\ ( fl_expr (Expr_function pattern_matching) = (fl_pattern_matching pattern_matching)) /\ ( fl_expr (Expr_try expr pattern_matching) = (fl_expr expr) ++ (fl_pattern_matching pattern_matching)) /\ ( fl_expr (Expr_let let_binding expr) = (fl_let_binding let_binding) ++ (fl_expr expr)) /\ ( fl_expr (Expr_letrec letrec_bindings expr) = (fl_letrec_bindings letrec_bindings) ++ (fl_expr expr)) /\ ( fl_expr (Expr_assert expr) = (fl_expr expr)) /\ ( fl_expr (Expr_location location) = [location]) `; val _ = ottDefine "ftv_definition" ` ( ftv_definition (D_let let_binding) = (ftv_let_binding let_binding)) /\ ( ftv_definition (D_letrec letrec_bindings) = (ftv_letrec_bindings letrec_bindings)) /\ ( ftv_definition (D_type type_definition) = (ftv_type_definition type_definition)) /\ ( ftv_definition (D_exception exception_definition) = (ftv_exception_definition exception_definition)) `; val _ = ottDefine "fv_definition" ` ( fv_definition (D_let let_binding) = (fv_let_binding let_binding)) /\ ( fv_definition (D_letrec letrec_bindings) = (list_minus (fv_letrec_bindings letrec_bindings) (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings))) /\ ( fv_definition (D_type type_definition) = []) /\ ( fv_definition (D_exception exception_definition) = []) `; val _ = ottDefine "fl_definition" ` ( fl_definition (D_let let_binding) = (fl_let_binding let_binding)) /\ ( fl_definition (D_letrec letrec_bindings) = (fl_letrec_bindings letrec_bindings)) /\ ( fl_definition (D_type type_definition) = []) /\ ( fl_definition (D_exception exception_definition) = []) `; val _ = ottDefine "ftv_definitions" ` ( ftv_definitions Ds_nil = []) /\ ( ftv_definitions (Ds_cons definition definitions) = (ftv_definition definition) ++ (ftv_definitions definitions)) `; val _ = ottDefine "ftv_typescheme" ` ( ftv_typescheme (TS_forall typexpr) = (ftv_typexpr typexpr)) `; val _ = ottDefine "ftv_typexprs" ` ( ftv_typexprs (typexprs_inj (typexpr_list)) = (FLAT (MAP (\typexpr_. (ftv_typexpr typexpr_)) typexpr_list))) `; val _ = ottDefine "fv_definitions" ` ( fv_definitions Ds_nil = []) /\ ( fv_definitions (Ds_cons definition definitions) = (fv_definition definition) ++ (list_minus (fv_definitions definitions) (aux_xs_definition_of_definition definition))) `; val _ = ottDefine "fl_definitions" ` ( fl_definitions Ds_nil = []) /\ ( fl_definitions (Ds_cons definition definitions) = (fl_definition definition) ++ (fl_definitions definitions)) `; val _ = ottDefine "ftv_substs_x" ` ( ftv_substs_x (substs_x_xs (value_name_expr_list)) = (FLAT (MAP (\(value_name_,expr_). (ftv_expr expr_)) value_name_expr_list))) `; val _ = ottDefine "ftv_program" ` ( ftv_program (Prog_defs definitions) = (ftv_definitions definitions)) /\ ( ftv_program (Prog_raise expr) = (ftv_expr expr)) `; val _ = ottDefine "ftv_environment_binding" ` ( ftv_environment_binding EB_tv = []) /\ ( ftv_environment_binding (EB_vn value_name typescheme) = (ftv_typescheme typescheme)) /\ ( ftv_environment_binding (EB_cc constr_name typeconstr) = []) /\ ( ftv_environment_binding (EB_pc constr_name type_params_opt typexprs typeconstr) = (list_minus (ftv_typexprs typexprs) (aux_typevars_type_params_opt_of_type_params_opt type_params_opt))) /\ ( ftv_environment_binding (EB_fn field_name type_params_opt typeconstr_name typexpr) = (list_minus (ftv_typexpr typexpr) (aux_typevars_type_params_opt_of_type_params_opt type_params_opt))) /\ ( ftv_environment_binding (EB_td typeconstr_name kind) = []) /\ ( ftv_environment_binding (EB_tr typeconstr_name kind (field_name_list)) = []) /\ ( ftv_environment_binding (EB_ta type_params_opt typeconstr_name typexpr) = (list_minus (ftv_typexpr typexpr) (aux_typevars_type_params_opt_of_type_params_opt type_params_opt))) /\ ( ftv_environment_binding (EB_l location typexpr) = (ftv_typexpr typexpr)) `; val _ = ottDefine "ftv_trans_label" ` ( ftv_trans_label Lab_nil = []) /\ ( ftv_trans_label (Lab_alloc v location) = []) /\ ( ftv_trans_label (Lab_deref location v) = []) /\ ( ftv_trans_label (Lab_assign location v) = []) `; val _ = ottDefine "fv_substs_x" ` ( fv_substs_x (substs_x_xs (value_name_expr_list)) = (FLAT (MAP (\(value_name_,expr_). (fv_expr expr_)) value_name_expr_list))) `; val _ = ottDefine "fv_program" ` ( fv_program (Prog_defs definitions) = (fv_definitions definitions)) /\ ( fv_program (Prog_raise expr) = (fv_expr expr)) `; val _ = ottDefine "fv_trans_label" ` ( fv_trans_label Lab_nil = []) /\ ( fv_trans_label (Lab_alloc v location) = []) /\ ( fv_trans_label (Lab_deref location v) = []) /\ ( fv_trans_label (Lab_assign location v) = []) `; val _ = ottDefine "fl_substs_x" ` ( fl_substs_x (substs_x_xs (value_name_expr_list)) = (FLAT (MAP (\(value_name_,expr_). (fl_expr expr_)) value_name_expr_list))) `; val _ = ottDefine "fl_program" ` ( fl_program (Prog_defs definitions) = (fl_definitions definitions)) /\ ( fl_program (Prog_raise expr) = (fl_expr expr)) `; val _ = ottDefine "fl_trans_label" ` ( fl_trans_label Lab_nil = []) /\ ( fl_trans_label (Lab_alloc v location) = []) /\ ( fl_trans_label (Lab_deref location v) = []) /\ ( fl_trans_label (Lab_assign location v) = []) `; (** substitutions *) val _ = ottDefine "substs_typevar_typexpr" ` ( substs_typevar_typexpr sub (TE_var typevar) = (case list_assoc typevar sub of NONE -> (TE_var typevar) || SOME t_5 -> t_5)) /\ ( substs_typevar_typexpr sub (TE_idxvar idx num) = TE_idxvar idx num) /\ ( substs_typevar_typexpr sub TE_any = TE_any ) /\ ( substs_typevar_typexpr sub (TE_arrow typexpr1 typexpr2) = TE_arrow (substs_typevar_typexpr sub typexpr1) (substs_typevar_typexpr sub typexpr2)) /\ ( substs_typevar_typexpr sub (TE_tuple (typexpr_list)) = TE_tuple (MAP (\typexpr_. (substs_typevar_typexpr sub typexpr_)) typexpr_list)) /\ ( substs_typevar_typexpr sub (TE_constr (typexpr_list) typeconstr) = TE_constr (MAP (\typexpr_. (substs_typevar_typexpr sub typexpr_)) typexpr_list) typeconstr) `; val _ = ottDefine "substs_typevar_constr_decl" ` ( substs_typevar_constr_decl sub (CD_nullary constr_name) = CD_nullary constr_name) /\ ( substs_typevar_constr_decl sub (CD_nary constr_name (typexpr_list)) = CD_nary constr_name (MAP (\typexpr_. (substs_typevar_typexpr sub typexpr_)) typexpr_list)) `; val _ = ottDefine "substs_typevar_field_decl" ` ( substs_typevar_field_decl sub (FD_immutable field_name typexpr) = FD_immutable field_name (substs_typevar_typexpr sub typexpr)) `; val _ = ottDefine "substs_typevar_type_equation" ` ( substs_typevar_type_equation sub (TE_te typexpr) = TE_te (substs_typevar_typexpr sub typexpr)) `; val _ = ottDefine "substs_typevar_type_representation" ` ( substs_typevar_type_representation sub (TR_variant (constr_decl_list)) = TR_variant (MAP (\constr_decl_. (substs_typevar_constr_decl sub constr_decl_)) constr_decl_list)) /\ ( substs_typevar_type_representation sub (TR_record (field_decl_list)) = TR_record (MAP (\field_decl_. (substs_typevar_field_decl sub field_decl_)) field_decl_list)) `; val _ = ottDefine "substs_typevar_type_information" ` ( substs_typevar_type_information sub (TI_eq type_equation) = TI_eq (substs_typevar_type_equation sub type_equation)) /\ ( substs_typevar_type_information sub (TI_def type_representation) = TI_def (substs_typevar_type_representation sub type_representation)) `; val _ = ottDefine "substs_typevar_pattern" ` ( substs_typevar_pattern sub (P_var value_name) = P_var value_name) /\ ( substs_typevar_pattern sub P_any = P_any ) /\ ( substs_typevar_pattern sub (P_constant constant) = P_constant constant) /\ ( substs_typevar_pattern sub (P_alias pattern value_name) = P_alias (substs_typevar_pattern sub pattern) value_name) /\ ( substs_typevar_pattern sub (P_typed pattern typexpr) = P_typed (substs_typevar_pattern sub pattern) (substs_typevar_typexpr sub typexpr)) /\ ( substs_typevar_pattern sub (P_or pattern1 pattern2) = P_or (substs_typevar_pattern sub pattern1) (substs_typevar_pattern sub pattern2)) /\ ( substs_typevar_pattern sub (P_construct constr (pattern_list)) = P_construct constr (MAP (\pattern_. (substs_typevar_pattern sub pattern_)) pattern_list)) /\ ( substs_typevar_pattern sub (P_construct_any constr) = P_construct_any constr) /\ ( substs_typevar_pattern sub (P_tuple (pattern_list)) = P_tuple (MAP (\pattern_. (substs_typevar_pattern sub pattern_)) pattern_list)) /\ ( substs_typevar_pattern sub (P_record (field_pattern_list)) = P_record (MAP (\(field_,pattern_). (field_,(substs_typevar_pattern sub pattern_))) field_pattern_list)) /\ ( substs_typevar_pattern sub (P_cons pattern1 pattern2) = P_cons (substs_typevar_pattern sub pattern1) (substs_typevar_pattern sub pattern2)) `; val _ = ottDefine "substs_typevar_typedef" ` ( substs_typevar_typedef sub (TD_td type_params_opt typeconstr_name type_information) = TD_td type_params_opt typeconstr_name (substs_typevar_type_information (FILTER (\(tv5,t5). ~(MEM tv5 (aux_typevars_type_params_opt_of_type_params_opt type_params_opt))) sub) type_information)) `; val _ = ottDefine "substs_typevar_letrec_binding" ` ( substs_typevar_letrec_binding sub (LRB_simple value_name pattern_matching) = LRB_simple value_name (substs_typevar_pattern_matching sub pattern_matching)) /\ ( substs_typevar_letrec_bindings sub (LRBs_inj (letrec_binding_list)) = LRBs_inj (MAP (\letrec_binding_. (substs_typevar_letrec_binding sub letrec_binding_)) letrec_binding_list)) /\ ( substs_typevar_let_binding sub (LB_simple pattern expr) = LB_simple (substs_typevar_pattern sub pattern) (substs_typevar_expr sub expr)) /\ ( substs_typevar_pat_exp sub (PE_inj pattern expr) = PE_inj (substs_typevar_pattern sub pattern) (substs_typevar_expr sub expr)) /\ ( substs_typevar_pattern_matching sub (PM_pm (pat_exp_list)) = PM_pm (MAP (\pat_exp_. (substs_typevar_pat_exp sub pat_exp_)) pat_exp_list)) /\ ( substs_typevar_expr sub (Expr_uprim unary_prim) = Expr_uprim unary_prim) /\ ( substs_typevar_expr sub (Expr_bprim binary_prim) = Expr_bprim binary_prim) /\ ( substs_typevar_expr sub (Expr_ident value_name) = Expr_ident value_name) /\ ( substs_typevar_expr sub (Expr_constant constant) = Expr_constant constant) /\ ( substs_typevar_expr sub (Expr_typed expr typexpr) = Expr_typed (substs_typevar_expr sub expr) (substs_typevar_typexpr sub typexpr)) /\ ( substs_typevar_expr sub (Expr_tuple (expr_list)) = Expr_tuple (MAP (\expr_. (substs_typevar_expr sub expr_)) expr_list)) /\ ( substs_typevar_expr sub (Expr_construct constr (expr_list)) = Expr_construct constr (MAP (\expr_. (substs_typevar_expr sub expr_)) expr_list)) /\ ( substs_typevar_expr sub (Expr_cons expr1 expr2) = Expr_cons (substs_typevar_expr sub expr1) (substs_typevar_expr sub expr2)) /\ ( substs_typevar_expr sub (Expr_record (field_expr_list)) = Expr_record (MAP (\(field_,expr_). (field_,(substs_typevar_expr sub expr_))) field_expr_list)) /\ ( substs_typevar_expr sub (Expr_override expr (field_expr_list)) = Expr_override (substs_typevar_expr sub expr) (MAP (\(field_,expr_). (field_,(substs_typevar_expr sub expr_))) field_expr_list)) /\ ( substs_typevar_expr sub (Expr_apply expr1 expr2) = Expr_apply (substs_typevar_expr sub expr1) (substs_typevar_expr sub expr2)) /\ ( substs_typevar_expr sub (Expr_and expr1 expr2) = Expr_and (substs_typevar_expr sub expr1) (substs_typevar_expr sub expr2)) /\ ( substs_typevar_expr sub (Expr_or expr1 expr2) = Expr_or (substs_typevar_expr sub expr1) (substs_typevar_expr sub expr2)) /\ ( substs_typevar_expr sub (Expr_field expr field) = Expr_field (substs_typevar_expr sub expr) field) /\ ( substs_typevar_expr sub (Expr_ifthenelse expr0 expr1 expr2) = Expr_ifthenelse (substs_typevar_expr sub expr0) (substs_typevar_expr sub expr1) (substs_typevar_expr sub expr2)) /\ ( substs_typevar_expr sub (Expr_while expr1 expr2) = Expr_while (substs_typevar_expr sub expr1) (substs_typevar_expr sub expr2)) /\ ( substs_typevar_expr sub (Expr_for x expr1 for_dirn expr2 expr3) = Expr_for x (substs_typevar_expr sub expr1) for_dirn (substs_typevar_expr sub expr2) (substs_typevar_expr sub expr3)) /\ ( substs_typevar_expr sub (Expr_sequence expr1 expr2) = Expr_sequence (substs_typevar_expr sub expr1) (substs_typevar_expr sub expr2)) /\ ( substs_typevar_expr sub (Expr_match expr pattern_matching) = Expr_match (substs_typevar_expr sub expr) (substs_typevar_pattern_matching sub pattern_matching)) /\ ( substs_typevar_expr sub (Expr_function pattern_matching) = Expr_function (substs_typevar_pattern_matching sub pattern_matching)) /\ ( substs_typevar_expr sub (Expr_try expr pattern_matching) = Expr_try (substs_typevar_expr sub expr) (substs_typevar_pattern_matching sub pattern_matching)) /\ ( substs_typevar_expr sub (Expr_let let_binding expr) = Expr_let (substs_typevar_let_binding sub let_binding) (substs_typevar_expr sub expr)) /\ ( substs_typevar_expr sub (Expr_letrec letrec_bindings expr) = Expr_letrec (substs_typevar_letrec_bindings sub letrec_bindings) (substs_typevar_expr sub expr)) /\ ( substs_typevar_expr sub (Expr_assert expr) = Expr_assert (substs_typevar_expr sub expr)) /\ ( substs_typevar_expr sub (Expr_location location) = Expr_location location) `; val _ = ottDefine "substs_typevar_type_definition" ` ( substs_typevar_type_definition sub (TDF_tdf (typedef_list)) = TDF_tdf (MAP (\typedef_. (substs_typevar_typedef sub typedef_)) typedef_list)) `; val _ = ottDefine "substs_typevar_exception_definition" ` ( substs_typevar_exception_definition sub (ED_def constr_decl) = ED_def (substs_typevar_constr_decl sub constr_decl)) `; val _ = ottDefine "substs_value_name_letrec_binding" ` ( substs_value_name_letrec_binding sub (LRB_simple value_name pattern_matching) = LRB_simple value_name (substs_value_name_pattern_matching sub pattern_matching)) /\ ( substs_value_name_letrec_bindings sub (LRBs_inj (letrec_binding_list)) = LRBs_inj (MAP (\letrec_binding_. (substs_value_name_letrec_binding sub letrec_binding_)) letrec_binding_list)) /\ ( substs_value_name_let_binding sub (LB_simple pattern expr) = LB_simple pattern (substs_value_name_expr sub expr)) /\ ( substs_value_name_pat_exp sub (PE_inj pattern expr) = PE_inj pattern (substs_value_name_expr (FILTER (\(x5,e5). ~(MEM x5 (aux_xs_pattern_of_pattern pattern))) sub) expr)) /\ ( substs_value_name_pattern_matching sub (PM_pm (pat_exp_list)) = PM_pm (MAP (\pat_exp_. (substs_value_name_pat_exp sub pat_exp_)) pat_exp_list)) /\ ( substs_value_name_expr sub (Expr_uprim unary_prim) = Expr_uprim unary_prim) /\ ( substs_value_name_expr sub (Expr_bprim binary_prim) = Expr_bprim binary_prim) /\ ( substs_value_name_expr sub (Expr_ident value_name) = (case list_assoc value_name sub of NONE -> (Expr_ident value_name) || SOME e5 -> e5)) /\ ( substs_value_name_expr sub (Expr_constant constant) = Expr_constant constant) /\ ( substs_value_name_expr sub (Expr_typed expr typexpr) = Expr_typed (substs_value_name_expr sub expr) typexpr) /\ ( substs_value_name_expr sub (Expr_tuple (expr_list)) = Expr_tuple (MAP (\expr_. (substs_value_name_expr sub expr_)) expr_list)) /\ ( substs_value_name_expr sub (Expr_construct constr (expr_list)) = Expr_construct constr (MAP (\expr_. (substs_value_name_expr sub expr_)) expr_list)) /\ ( substs_value_name_expr sub (Expr_cons expr1 expr2) = Expr_cons (substs_value_name_expr sub expr1) (substs_value_name_expr sub expr2)) /\ ( substs_value_name_expr sub (Expr_record (field_expr_list)) = Expr_record (MAP (\(field_,expr_). (field_,(substs_value_name_expr sub expr_))) field_expr_list)) /\ ( substs_value_name_expr sub (Expr_override expr (field_expr_list)) = Expr_override (substs_value_name_expr sub expr) (MAP (\(field_,expr_). (field_,(substs_value_name_expr sub expr_))) field_expr_list)) /\ ( substs_value_name_expr sub (Expr_apply expr1 expr2) = Expr_apply (substs_value_name_expr sub expr1) (substs_value_name_expr sub expr2)) /\ ( substs_value_name_expr sub (Expr_and expr1 expr2) = Expr_and (substs_value_name_expr sub expr1) (substs_value_name_expr sub expr2)) /\ ( substs_value_name_expr sub (Expr_or expr1 expr2) = Expr_or (substs_value_name_expr sub expr1) (substs_value_name_expr sub expr2)) /\ ( substs_value_name_expr sub (Expr_field expr field) = Expr_field (substs_value_name_expr sub expr) field) /\ ( substs_value_name_expr sub (Expr_ifthenelse expr0 expr1 expr2) = Expr_ifthenelse (substs_value_name_expr sub expr0) (substs_value_name_expr sub expr1) (substs_value_name_expr sub expr2)) /\ ( substs_value_name_expr sub (Expr_while expr1 expr2) = Expr_while (substs_value_name_expr sub expr1) (substs_value_name_expr sub expr2)) /\ ( substs_value_name_expr sub (Expr_for x expr1 for_dirn expr2 expr3) = Expr_for x (substs_value_name_expr sub expr1) for_dirn (substs_value_name_expr sub expr2) (substs_value_name_expr (FILTER (\(x5,e5). ~(MEM x5 [x])) sub) expr3)) /\ ( substs_value_name_expr sub (Expr_sequence expr1 expr2) = Expr_sequence (substs_value_name_expr sub expr1) (substs_value_name_expr sub expr2)) /\ ( substs_value_name_expr sub (Expr_match expr pattern_matching) = Expr_match (substs_value_name_expr sub expr) (substs_value_name_pattern_matching sub pattern_matching)) /\ ( substs_value_name_expr sub (Expr_function pattern_matching) = Expr_function (substs_value_name_pattern_matching sub pattern_matching)) /\ ( substs_value_name_expr sub (Expr_try expr pattern_matching) = Expr_try (substs_value_name_expr sub expr) (substs_value_name_pattern_matching sub pattern_matching)) /\ ( substs_value_name_expr sub (Expr_let let_binding expr) = Expr_let (substs_value_name_let_binding sub let_binding) (substs_value_name_expr (FILTER (\(x5,e5). ~(MEM x5 (aux_xs_let_binding_of_let_binding let_binding))) sub) expr)) /\ ( substs_value_name_expr sub (Expr_letrec letrec_bindings expr) = Expr_letrec (substs_value_name_letrec_bindings (FILTER (\(x5,e5). ~(MEM x5 (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings))) sub) letrec_bindings) (substs_value_name_expr (FILTER (\(x5,e5). ~(MEM x5 (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings))) sub) expr)) /\ ( substs_value_name_expr sub (Expr_assert expr) = Expr_assert (substs_value_name_expr sub expr)) /\ ( substs_value_name_expr sub (Expr_location location) = Expr_location location) `; val _ = ottDefine "subst_value_name_letrec_binding" ` ( subst_value_name_letrec_binding e5 x5 (LRB_simple value_name pattern_matching) = LRB_simple value_name (subst_value_name_pattern_matching e5 x5 pattern_matching)) /\ ( subst_value_name_letrec_bindings e5 x5 (LRBs_inj (letrec_binding_list)) = LRBs_inj (MAP (\letrec_binding_. (subst_value_name_letrec_binding e5 x5 letrec_binding_)) letrec_binding_list)) /\ ( subst_value_name_let_binding e5 x5 (LB_simple pattern expr) = LB_simple pattern (subst_value_name_expr e5 x5 expr)) /\ ( subst_value_name_pat_exp e5 x5 (PE_inj pattern expr) = PE_inj pattern (if MEM x5 (aux_xs_pattern_of_pattern pattern) then expr else (subst_value_name_expr e5 x5 expr))) /\ ( subst_value_name_pattern_matching e5 x5 (PM_pm (pat_exp_list)) = PM_pm (MAP (\pat_exp_. (subst_value_name_pat_exp e5 x5 pat_exp_)) pat_exp_list)) /\ ( subst_value_name_expr e5 x5 (Expr_uprim unary_prim) = Expr_uprim unary_prim) /\ ( subst_value_name_expr e5 x5 (Expr_bprim binary_prim) = Expr_bprim binary_prim) /\ ( subst_value_name_expr e5 x5 (Expr_ident value_name) = (if value_name=x5 then e5 else (Expr_ident value_name))) /\ ( subst_value_name_expr e5 x5 (Expr_constant constant) = Expr_constant constant) /\ ( subst_value_name_expr e5 x5 (Expr_typed expr typexpr) = Expr_typed (subst_value_name_expr e5 x5 expr) typexpr) /\ ( subst_value_name_expr e5 x5 (Expr_tuple (expr_list)) = Expr_tuple (MAP (\expr_. (subst_value_name_expr e5 x5 expr_)) expr_list)) /\ ( subst_value_name_expr e5 x5 (Expr_construct constr (expr_list)) = Expr_construct constr (MAP (\expr_. (subst_value_name_expr e5 x5 expr_)) expr_list)) /\ ( subst_value_name_expr e5 x5 (Expr_cons expr1 expr2) = Expr_cons (subst_value_name_expr e5 x5 expr1) (subst_value_name_expr e5 x5 expr2)) /\ ( subst_value_name_expr e5 x5 (Expr_record (field_expr_list)) = Expr_record (MAP (\(field_,expr_). (field_,(subst_value_name_expr e5 x5 expr_))) field_expr_list)) /\ ( subst_value_name_expr e5 x5 (Expr_override expr (field_expr_list)) = Expr_override (subst_value_name_expr e5 x5 expr) (MAP (\(field_,expr_). (field_,(subst_value_name_expr e5 x5 expr_))) field_expr_list)) /\ ( subst_value_name_expr e5 x5 (Expr_apply expr1 expr2) = Expr_apply (subst_value_name_expr e5 x5 expr1) (subst_value_name_expr e5 x5 expr2)) /\ ( subst_value_name_expr e5 x5 (Expr_and expr1 expr2) = Expr_and (subst_value_name_expr e5 x5 expr1) (subst_value_name_expr e5 x5 expr2)) /\ ( subst_value_name_expr e5 x5 (Expr_or expr1 expr2) = Expr_or (subst_value_name_expr e5 x5 expr1) (subst_value_name_expr e5 x5 expr2)) /\ ( subst_value_name_expr e5 x5 (Expr_field expr field) = Expr_field (subst_value_name_expr e5 x5 expr) field) /\ ( subst_value_name_expr e5 x5 (Expr_ifthenelse expr0 expr1 expr2) = Expr_ifthenelse (subst_value_name_expr e5 x5 expr0) (subst_value_name_expr e5 x5 expr1) (subst_value_name_expr e5 x5 expr2)) /\ ( subst_value_name_expr e5 x5 (Expr_while expr1 expr2) = Expr_while (subst_value_name_expr e5 x5 expr1) (subst_value_name_expr e5 x5 expr2)) /\ ( subst_value_name_expr e5 x5 (Expr_for x expr1 for_dirn expr2 expr3) = Expr_for x (subst_value_name_expr e5 x5 expr1) for_dirn (subst_value_name_expr e5 x5 expr2) (if MEM x5 [x] then expr3 else (subst_value_name_expr e5 x5 expr3))) /\ ( subst_value_name_expr e5 x5 (Expr_sequence expr1 expr2) = Expr_sequence (subst_value_name_expr e5 x5 expr1) (subst_value_name_expr e5 x5 expr2)) /\ ( subst_value_name_expr e5 x5 (Expr_match expr pattern_matching) = Expr_match (subst_value_name_expr e5 x5 expr) (subst_value_name_pattern_matching e5 x5 pattern_matching)) /\ ( subst_value_name_expr e5 x5 (Expr_function pattern_matching) = Expr_function (subst_value_name_pattern_matching e5 x5 pattern_matching)) /\ ( subst_value_name_expr e5 x5 (Expr_try expr pattern_matching) = Expr_try (subst_value_name_expr e5 x5 expr) (subst_value_name_pattern_matching e5 x5 pattern_matching)) /\ ( subst_value_name_expr e5 x5 (Expr_let let_binding expr) = Expr_let (subst_value_name_let_binding e5 x5 let_binding) (if MEM x5 (aux_xs_let_binding_of_let_binding let_binding) then expr else (subst_value_name_expr e5 x5 expr))) /\ ( subst_value_name_expr e5 x5 (Expr_letrec letrec_bindings expr) = Expr_letrec (if MEM x5 (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings) then letrec_bindings else (subst_value_name_letrec_bindings e5 x5 letrec_bindings)) (if MEM x5 (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings) then expr else (subst_value_name_expr e5 x5 expr))) /\ ( subst_value_name_expr e5 x5 (Expr_assert expr) = Expr_assert (subst_value_name_expr e5 x5 expr)) /\ ( subst_value_name_expr e5 x5 (Expr_location location) = Expr_location location) `; val _ = ottDefine "substs_typevar_definition" ` ( substs_typevar_definition sub (D_let let_binding) = D_let (substs_typevar_let_binding sub let_binding)) /\ ( substs_typevar_definition sub (D_letrec letrec_bindings) = D_letrec (substs_typevar_letrec_bindings sub letrec_bindings)) /\ ( substs_typevar_definition sub (D_type type_definition) = D_type (substs_typevar_type_definition sub type_definition)) /\ ( substs_typevar_definition sub (D_exception exception_definition) = D_exception (substs_typevar_exception_definition sub exception_definition)) `; val _ = ottDefine "substs_value_name_definition" ` ( substs_value_name_definition sub (D_let let_binding) = D_let (substs_value_name_let_binding sub let_binding)) /\ ( substs_value_name_definition sub (D_letrec letrec_bindings) = D_letrec (substs_value_name_letrec_bindings (FILTER (\(x5,e5). ~(MEM x5 (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings))) sub) letrec_bindings)) /\ ( substs_value_name_definition sub (D_type type_definition) = D_type type_definition) /\ ( substs_value_name_definition sub (D_exception exception_definition) = D_exception exception_definition) `; val _ = ottDefine "subst_value_name_definition" ` ( subst_value_name_definition e5 x5 (D_let let_binding) = D_let (subst_value_name_let_binding e5 x5 let_binding)) /\ ( subst_value_name_definition e5 x5 (D_letrec letrec_bindings) = D_letrec (if MEM x5 (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings) then letrec_bindings else (subst_value_name_letrec_bindings e5 x5 letrec_bindings))) /\ ( subst_value_name_definition e5 x5 (D_type type_definition) = D_type type_definition) /\ ( subst_value_name_definition e5 x5 (D_exception exception_definition) = D_exception exception_definition) `; val _ = ottDefine "substs_typevar_definitions" ` ( substs_typevar_definitions sub Ds_nil = Ds_nil ) /\ ( substs_typevar_definitions sub (Ds_cons definition definitions) = Ds_cons (substs_typevar_definition sub definition) (substs_typevar_definitions sub definitions)) `; val _ = ottDefine "substs_typevar_typescheme" ` ( substs_typevar_typescheme sub (TS_forall typexpr) = TS_forall (substs_typevar_typexpr sub typexpr)) `; val _ = ottDefine "substs_typevar_typexprs" ` ( substs_typevar_typexprs sub (typexprs_inj (typexpr_list)) = typexprs_inj (MAP (\typexpr_. (substs_typevar_typexpr sub typexpr_)) typexpr_list)) `; val _ = ottDefine "substs_value_name_definitions" ` ( substs_value_name_definitions sub Ds_nil = Ds_nil ) /\ ( substs_value_name_definitions sub (Ds_cons definition definitions) = Ds_cons (substs_value_name_definition sub definition) (substs_value_name_definitions (FILTER (\(x5,e5). ~(MEM x5 (aux_xs_definition_of_definition definition))) sub) definitions)) `; val _ = ottDefine "subst_value_name_definitions" ` ( subst_value_name_definitions e5 x5 Ds_nil = Ds_nil ) /\ ( subst_value_name_definitions e5 x5 (Ds_cons definition definitions) = Ds_cons (subst_value_name_definition e5 x5 definition) (if MEM x5 (aux_xs_definition_of_definition definition) then definitions else (subst_value_name_definitions e5 x5 definitions))) `; val _ = ottDefine "substs_typevar_substs_x" ` ( substs_typevar_substs_x sub (substs_x_xs (value_name_expr_list)) = substs_x_xs (MAP (\(value_name_,expr_). (value_name_,(substs_typevar_expr sub expr_))) value_name_expr_list)) `; val _ = ottDefine "substs_typevar_program" ` ( substs_typevar_program sub (Prog_defs definitions) = Prog_defs (substs_typevar_definitions sub definitions)) /\ ( substs_typevar_program sub (Prog_raise expr) = Prog_raise (substs_typevar_expr sub expr)) `; val _ = ottDefine "substs_typevar_environment_binding" ` ( substs_typevar_environment_binding sub EB_tv = EB_tv ) /\ ( substs_typevar_environment_binding sub (EB_vn value_name typescheme) = EB_vn value_name (substs_typevar_typescheme sub typescheme)) /\ ( substs_typevar_environment_binding sub (EB_cc constr_name typeconstr) = EB_cc constr_name typeconstr) /\ ( substs_typevar_environment_binding sub (EB_pc constr_name type_params_opt typexprs typeconstr) = EB_pc constr_name type_params_opt (substs_typevar_typexprs (FILTER (\(tv5,t5). ~(MEM tv5 (aux_typevars_type_params_opt_of_type_params_opt type_params_opt))) sub) typexprs) typeconstr) /\ ( substs_typevar_environment_binding sub (EB_fn field_name type_params_opt typeconstr_name typexpr) = EB_fn field_name type_params_opt typeconstr_name (substs_typevar_typexpr (FILTER (\(tv5,t5). ~(MEM tv5 (aux_typevars_type_params_opt_of_type_params_opt type_params_opt))) sub) typexpr)) /\ ( substs_typevar_environment_binding sub (EB_td typeconstr_name kind) = EB_td typeconstr_name kind) /\ ( substs_typevar_environment_binding sub (EB_tr typeconstr_name kind (field_name_list)) = EB_tr typeconstr_name kind field_name_list) /\ ( substs_typevar_environment_binding sub (EB_ta type_params_opt typeconstr_name typexpr) = EB_ta type_params_opt typeconstr_name (substs_typevar_typexpr (FILTER (\(tv5,t5). ~(MEM tv5 (aux_typevars_type_params_opt_of_type_params_opt type_params_opt))) sub) typexpr)) /\ ( substs_typevar_environment_binding sub (EB_l location typexpr) = EB_l location (substs_typevar_typexpr sub typexpr)) `; val _ = ottDefine "substs_typevar_trans_label" ` ( substs_typevar_trans_label sub Lab_nil = Lab_nil ) /\ ( substs_typevar_trans_label sub (Lab_alloc v location) = Lab_alloc v location) /\ ( substs_typevar_trans_label sub (Lab_deref location v) = Lab_deref location v) /\ ( substs_typevar_trans_label sub (Lab_assign location v) = Lab_assign location v) `; val _ = ottDefine "substs_value_name_substs_x" ` ( substs_value_name_substs_x sub (substs_x_xs (value_name_expr_list)) = substs_x_xs (MAP (\(value_name_,expr_). (value_name_,(substs_value_name_expr sub expr_))) value_name_expr_list)) `; val _ = ottDefine "substs_value_name_program" ` ( substs_value_name_program sub (Prog_defs definitions) = Prog_defs (substs_value_name_definitions sub definitions)) /\ ( substs_value_name_program sub (Prog_raise expr) = Prog_raise (substs_value_name_expr sub expr)) `; val _ = ottDefine "substs_value_name_trans_label" ` ( substs_value_name_trans_label sub Lab_nil = Lab_nil ) /\ ( substs_value_name_trans_label sub (Lab_alloc v location) = Lab_alloc v location) /\ ( substs_value_name_trans_label sub (Lab_deref location v) = Lab_deref location v) /\ ( substs_value_name_trans_label sub (Lab_assign location v) = Lab_assign location v) `; val _ = ottDefine "subst_value_name_substs_x" ` ( subst_value_name_substs_x e5 x5 (substs_x_xs (value_name_expr_list)) = substs_x_xs (MAP (\(value_name_,expr_). (value_name_,(subst_value_name_expr e5 x5 expr_))) value_name_expr_list)) `; val _ = ottDefine "subst_value_name_program" ` ( subst_value_name_program e5 x5 (Prog_defs definitions) = Prog_defs (subst_value_name_definitions e5 x5 definitions)) /\ ( subst_value_name_program e5 x5 (Prog_raise expr) = Prog_raise (subst_value_name_expr e5 x5 expr)) `; val _ = ottDefine "subst_value_name_trans_label" ` ( subst_value_name_trans_label e5 x5 Lab_nil = Lab_nil ) /\ ( subst_value_name_trans_label e5 x5 (Lab_alloc v location) = Lab_alloc v location) /\ ( subst_value_name_trans_label e5 x5 (Lab_deref location v) = Lab_deref location v) /\ ( subst_value_name_trans_label e5 x5 (Lab_assign location v) = Lab_assign location v) `; val _ = Define `fold_pat pats expr = FOLDR (\p e. Expr_function (PM_pm [PE_inj p e])) expr pats`; val _ = ottDefine "shiftt" `( (shiftt m n (TE_var typevar) ) = (TE_var typevar)) /\ ( (shiftt m n (TE_idxvar idx num) ) = if ( idx < m ) then (TE_idxvar idx num) else (TE_idxvar ( idx + n ) num)) /\ ( (shiftt m n TE_any ) = TE_any) /\ ( (shiftt m n (TE_arrow typexpr1 typexpr2) ) = (TE_arrow (shiftt m n typexpr1 ) (shiftt m n typexpr2 ) )) /\ (shiftt m n (TE_tuple typexprs) = TE_tuple (MAP (shiftt m n) typexprs)) /\ (shiftt m n (TE_constr typexprs tc) = TE_constr (MAP (shiftt m n) typexprs) tc)`; val _ = Define `(shifttes m n (typexprs_inj tes) = typexprs_inj (MAP (shiftt m n) tes))`; val _ = Define `( (shiftts m n (TS_forall typexpr) ) = (TS_forall (shiftt ( m + 1 ) n typexpr ) ))`; val _ = Define `( (shiftEB m n EB_tv ) = EB_tv) /\ ( (shiftEB m n (EB_vn value_name typescheme) ) = (EB_vn value_name (shiftts m n typescheme ) )) /\ ( (shiftEB m n (EB_cc constr_name typeconstr) ) = (EB_cc constr_name typeconstr)) /\ ( (shiftEB m n (EB_pc constr_name type_params_opt typexprs typeconstr) ) = (EB_pc constr_name type_params_opt (shifttes m n typexprs ) typeconstr)) /\ ( (shiftEB m n (EB_fn field_name type_params_opt typeconstr_name typexpr) ) = (EB_fn field_name type_params_opt typeconstr_name (shiftt m n typexpr ) )) /\ ( (shiftEB m n (EB_td typeconstr_name kind) ) = (EB_td typeconstr_name kind)) /\ (shiftEB m n (EB_tr tcn k field_names) = EB_tr tcn k field_names) /\ ( (shiftEB m n (EB_ta type_params_opt typeconstr_name typexpr) ) = (EB_ta type_params_opt typeconstr_name (shiftt m n typexpr ) )) /\ ( (shiftEB m n (EB_l location typexpr) ) = (EB_l location (shiftt m n typexpr ) ))`; val num_tv_def = Define `(num_tv [] = 0:num) /\ (num_tv (EB_tv::E) = 1 + num_tv E) /\ (num_tv (EB::E) = num_tv E)`; val _ = Define `(shiftE m n [] = []) /\ (shiftE m n (EB::E) = shiftEB (m + num_tv E) n EB::shiftE m n E)`; val _ = Define `(shiftTsig m n Tsig = MAP (\(tv, t). (tv, shiftt m n t)) Tsig)`; val _ = Define `(definitions_snoc Ds_nil d = Ds_cons d Ds_nil) /\ (definitions_snoc (Ds_cons d ds) d' = Ds_cons d (definitions_snoc ds d'))`; val _ = ottDefine "remv_tyvar_typexpr" `(remv_tyvar_typexpr (TE_var typevar) = TE_any) /\ (remv_tyvar_typexpr (TE_idxvar idx num) = TE_idxvar idx num) /\ (remv_tyvar_typexpr TE_any = TE_any) /\ (remv_tyvar_typexpr (TE_arrow typexpr1 typexpr2) = TE_arrow (remv_tyvar_typexpr typexpr1) (remv_tyvar_typexpr typexpr2)) /\ (remv_tyvar_typexpr (TE_tuple (typexpr_list)) = TE_tuple (MAP (\typexpr_. (remv_tyvar_typexpr typexpr_)) typexpr_list)) /\ (remv_tyvar_typexpr (TE_constr (typexpr_list) typeconstr) = TE_constr (MAP (\typexpr_. (remv_tyvar_typexpr typexpr_)) typexpr_list) typeconstr)`; val _ = ottDefine "remv_tyvar_pattern" `(remv_tyvar_pattern (P_var value_name) = P_var value_name) /\ (remv_tyvar_pattern P_any = P_any) /\ (remv_tyvar_pattern (P_constant constant) = P_constant constant) /\ (remv_tyvar_pattern (P_alias pattern value_name) = P_alias (remv_tyvar_pattern pattern) value_name) /\ (remv_tyvar_pattern (P_typed pattern typexpr) = P_typed (remv_tyvar_pattern pattern) (remv_tyvar_typexpr typexpr)) /\ (remv_tyvar_pattern (P_or pattern1 pattern2) = P_or (remv_tyvar_pattern pattern1) (remv_tyvar_pattern pattern2)) /\ (remv_tyvar_pattern (P_construct constr (pattern_list)) = P_construct constr (MAP (\pattern_. (remv_tyvar_pattern pattern_)) pattern_list)) /\ (remv_tyvar_pattern (P_construct_any constr) = P_construct_any constr) /\ (remv_tyvar_pattern (P_tuple (pattern_list)) = P_tuple (MAP (\pattern_. (remv_tyvar_pattern pattern_)) pattern_list)) /\ (remv_tyvar_pattern (P_record (field_pattern_list)) = P_record (MAP (\(field_,pattern_). (field_,(remv_tyvar_pattern pattern_))) field_pattern_list)) /\ (remv_tyvar_pattern (P_cons pattern1 pattern2) = P_cons (remv_tyvar_pattern pattern1) (remv_tyvar_pattern pattern2))`; val _ = ottDefine "remv_tyvar_letrec_binding" `(remv_tyvar_letrec_binding (LRB_simple value_name pattern_matching) = LRB_simple value_name (remv_tyvar_pattern_matching pattern_matching)) /\ (remv_tyvar_letrec_bindings (LRBs_inj (letrec_binding_list)) = LRBs_inj (MAP (\letrec_binding_. (remv_tyvar_letrec_binding letrec_binding_)) letrec_binding_list)) /\ (remv_tyvar_let_binding (LB_simple pattern expr) = LB_simple (remv_tyvar_pattern pattern) (remv_tyvar_expr expr)) /\ (remv_tyvar_pat_exp (PE_inj pattern expr) = PE_inj (remv_tyvar_pattern pattern) (remv_tyvar_expr expr)) /\ (remv_tyvar_pattern_matching (PM_pm (pat_exp_list)) = PM_pm (MAP (\pat_exp_. (remv_tyvar_pat_exp pat_exp_)) pat_exp_list)) /\ (remv_tyvar_expr (Expr_uprim unary_prim) = Expr_uprim unary_prim) /\ (remv_tyvar_expr (Expr_bprim binary_prim) = Expr_bprim binary_prim) /\ (remv_tyvar_expr (Expr_ident value_name) = Expr_ident value_name) /\ (remv_tyvar_expr (Expr_constant constant) = Expr_constant constant) /\ (remv_tyvar_expr (Expr_typed expr typexpr) = Expr_typed (remv_tyvar_expr expr) (remv_tyvar_typexpr typexpr)) /\ (remv_tyvar_expr (Expr_tuple (expr_list)) = Expr_tuple (MAP (\expr_. (remv_tyvar_expr expr_)) expr_list)) /\ (remv_tyvar_expr (Expr_construct constr (expr_list)) = Expr_construct constr (MAP (\expr_. (remv_tyvar_expr expr_)) expr_list)) /\ (remv_tyvar_expr (Expr_cons expr1 expr2) = Expr_cons (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)) /\ (remv_tyvar_expr (Expr_record (field_expr_list)) = Expr_record (MAP (\(field_,expr_). (field_,(remv_tyvar_expr expr_))) field_expr_list)) /\ (remv_tyvar_expr (Expr_override expr (field_expr_list)) = Expr_override (remv_tyvar_expr expr) (MAP (\(field_,expr_). (field_,(remv_tyvar_expr expr_))) field_expr_list)) /\ (remv_tyvar_expr (Expr_apply expr1 expr2) = Expr_apply (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)) /\ (remv_tyvar_expr (Expr_and expr1 expr2) = Expr_and (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)) /\ (remv_tyvar_expr (Expr_or expr1 expr2) = Expr_or (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)) /\ (remv_tyvar_expr (Expr_field expr field) = Expr_field (remv_tyvar_expr expr) field) /\ (remv_tyvar_expr (Expr_ifthenelse expr0 expr1 expr2) = Expr_ifthenelse (remv_tyvar_expr expr0) (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)) /\ (remv_tyvar_expr (Expr_while expr1 expr2) = Expr_while (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)) /\ (remv_tyvar_expr (Expr_for x expr1 for_dirn expr2 expr3) = Expr_for x (remv_tyvar_expr expr1) for_dirn (remv_tyvar_expr expr2) (remv_tyvar_expr expr3))/\ (remv_tyvar_expr (Expr_sequence expr1 expr2) = Expr_sequence (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)) /\ (remv_tyvar_expr (Expr_match expr pattern_matching) = Expr_match (remv_tyvar_expr expr) (remv_tyvar_pattern_matching pattern_matching)) /\ (remv_tyvar_expr (Expr_function pattern_matching) = Expr_function (remv_tyvar_pattern_matching pattern_matching)) /\ (remv_tyvar_expr (Expr_try expr pattern_matching) = Expr_try (remv_tyvar_expr expr) (remv_tyvar_pattern_matching pattern_matching)) /\ (remv_tyvar_expr (Expr_let let_binding expr) = Expr_let (remv_tyvar_let_binding let_binding) (remv_tyvar_expr expr)) /\ (remv_tyvar_expr (Expr_letrec letrec_bindings expr) = Expr_letrec (remv_tyvar_letrec_bindings letrec_bindings) (remv_tyvar_expr expr)) /\ (remv_tyvar_expr (Expr_assert expr) = Expr_assert (remv_tyvar_expr expr)) /\ (remv_tyvar_expr (Expr_location location) = Expr_location location)`; (** definitions *) (* defns JdomEB *) val (JdomEB_rules, JdomEB_ind, JdomEB_cases) = Hol_reln ` (* defn domEB *) ( (* JdomEB_type_param *) (clause_name "JdomEB_type_param") ==> ( ( JdomEB EB_tv name_tv ))) /\ ( (* JdomEB_value_name *) !(value_name:value_name) (typescheme:typescheme) . (clause_name "JdomEB_value_name") ==> ( ( JdomEB (EB_vn value_name typescheme) (name_vn value_name) ))) /\ ( (* JdomEB_const_constr_name *) !(constr_name:constr_name) (typeconstr:typeconstr) . (clause_name "JdomEB_const_constr_name") ==> ( ( JdomEB (EB_cc constr_name typeconstr) (name_cn constr_name) ))) /\ ( (* JdomEB_constr_name *) !(t_list:typexpr list) (constr_name:constr_name) (type_params_opt:type_params_opt) (typeconstr:typeconstr) . (clause_name "JdomEB_constr_name") ==> ( ( JdomEB (EB_pc constr_name type_params_opt (typexprs_inj (t_list)) typeconstr) (name_cn constr_name) ))) /\ ( (* JdomEB_opaque_typeconstr_name *) !(typeconstr_name:typeconstr_name) (kind:kind) . (clause_name "JdomEB_opaque_typeconstr_name") ==> ( ( JdomEB (EB_td typeconstr_name kind) (name_tcn typeconstr_name) ))) /\ ( (* JdomEB_trans_typeconstr_name *) !(type_params_opt:type_params_opt) (typeconstr_name:typeconstr_name) (t:typexpr) . (clause_name "JdomEB_trans_typeconstr_name") ==> ( ( JdomEB (EB_ta type_params_opt typeconstr_name t) (name_tcn typeconstr_name) ))) /\ ( (* JdomEB_record_typeconstr_name *) !(field_name_list:field_name list) (typeconstr_name:typeconstr_name) (kind:kind) . (clause_name "JdomEB_record_typeconstr_name") ==> ( ( JdomEB (EB_tr typeconstr_name kind (field_name_list)) (name_tcn typeconstr_name) ))) /\ ( (* JdomEB_record_field_name *) !(field_name:field_name) (type_params_opt:type_params_opt) (typeconstr_name:typeconstr_name) (typexpr:typexpr) . (clause_name "JdomEB_record_field_name") ==> ( ( JdomEB (EB_fn field_name type_params_opt typeconstr_name typexpr) (name_fn field_name) ))) /\ ( (* JdomEB_location *) !(location:location) (t:typexpr) . (clause_name "JdomEB_location") ==> ( ( JdomEB (EB_l location t) (name_l location) ))) `; (* defns JdomE *) val (JdomE_rules, JdomE_ind, JdomE_cases) = Hol_reln ` (* defn domE *) ( (* JdomE_empty *) (clause_name "JdomE_empty") ==> ( ( JdomE [] NIL ))) /\ ( (* JdomE_cons *) !(name_list:name list) (E:environment) (EB:environment_binding) (name:name) . (clause_name "JdomE_cons") /\ (( ( JdomE E (name_list) )) /\ ( ( JdomEB EB name ))) ==> ( ( JdomE ( EB :: E ) ([(name)] ++ name_list) ))) `; (* defns Jlookup *) val (Jlookup_rules, Jlookup_ind, Jlookup_cases) = Hol_reln ` (* defn EB *) ( (* Jlookup_EB_rec1 *) !(E:environment) (EB:environment_binding) (name:name) (EB':environment_binding) (name':name) . (clause_name "Jlookup_EB_rec1") /\ (( ( JdomEB EB name' )) /\ ( (~( name = name' )) ) /\ ( (~( name' = name_tv )) ) /\ ( ( Jlookup_EB E name EB' ))) ==> ( ( Jlookup_EB ( EB :: E ) name EB' ))) /\ ( (* Jlookup_EB_rec2 *) !(E:environment) (name:name) (EB':environment_binding) . (clause_name "Jlookup_EB_rec2") /\ (( (~( name = name_tv )) ) /\ ( ( Jlookup_EB E name EB' ))) ==> ( ( Jlookup_EB ( EB_tv :: E ) name (shiftEB 0 1 EB' ) ))) /\ ( (* Jlookup_EB_head *) !(E:environment) (EB:environment_binding) (name:name) . (clause_name "Jlookup_EB_head") /\ (( ( JdomEB EB name ))) ==> ( ( Jlookup_EB ( EB :: E ) name EB ))) `; (* defns Jidx *) val (Jidx_rules, Jidx_ind, Jidx_cases) = Hol_reln ` (* defn bound *) ( (* Jidx_bound_skip1 *) !(E:environment) (EB:environment_binding) (idx:idx) (name:name) . (clause_name "Jidx_bound_skip1") /\ (( ( Jidx_bound E idx )) /\ ( ( JdomEB EB name )) /\ ( (~( name = name_tv )) )) ==> ( ( Jidx_bound ( EB :: E ) idx ))) /\ ( (* Jidx_bound_skip2 *) !(E:environment) (idx:idx) . (clause_name "Jidx_bound_skip2") /\ (( ( Jidx_bound E idx ))) ==> ( ( Jidx_bound ( EB_tv :: E ) ( idx + 1 ) ))) /\ ( (* Jidx_bound_found *) !(E:environment) . (clause_name "Jidx_bound_found") ==> ( ( Jidx_bound ( EB_tv :: E ) 0 ))) `; (* defns JTtps_kind *) val (JTtps_kind_rules, JTtps_kind_ind, JTtps_kind_cases) = Hol_reln ` (* defn tps_kind *) ( (* JTtps_kind_kind *) !(tp_list:type_param list) (n:index) . (clause_name "JTtps_kind_kind") /\ (( (ALL_DISTINCT ( (tp_list) )) ) /\ ( ( n = LENGTH ( (tp_list) )) )) ==> ( ( JTtps_kind (TPS_nary (tp_list)) n ))) `; (* defns JTEok *) val (JTEok_rules, JTEok_ind, JTEok_cases) = Hol_reln ` (* defn Eok *) ( (* JTEok_empty *) (clause_name "JTEok_empty") ==> ( ( JTEok [] ))) /\ ( (* JTEok_typevar *) !(E:environment) . (clause_name "JTEok_typevar") /\ (( ( JTEok E ))) ==> ( ( JTEok ( EB_tv :: E ) ))) /\ ( (* JTEok_value_name *) !(E:environment) (value_name:value_name) (t:typexpr) . (clause_name "JTEok_value_name") /\ (( ( JTts E (TS_forall t) 0 ))) ==> ( ( JTEok ( (EB_vn value_name (TS_forall t)) :: E ) ))) /\ ( (* JTEok_constr_name_c *) !(E:environment) (constr_name:constr_name) (typeconstr_name:typeconstr_name) (kind:kind) (names:names) . (clause_name "JTEok_constr_name_c") /\ (( ( JTEok E )) /\ ( ( Jlookup_EB E (name_tcn typeconstr_name) (EB_td typeconstr_name kind) )) /\ ( ( JdomE E names )) /\ ( (~MEM (name_cn constr_name) names ) )) ==> ( ( JTEok ( (EB_cc constr_name (TC_name typeconstr_name)) :: E ) ))) /\ ( (* JTEok_exn_constr_name_c *) !(E:environment) (constr_name:constr_name) (names:names) . (clause_name "JTEok_exn_constr_name_c") /\ (( ( JTEok E )) /\ ( ( JdomE E names )) /\ ( (~MEM (name_cn constr_name) names ) )) ==> ( ( JTEok ( (EB_cc constr_name TC_exn) :: E ) ))) /\ ( (* JTEok_constr_name_p *) !(t_list:typexpr list) (tv_list:typevar list) (E:environment) (constr_name:constr_name) (typeconstr_name:typeconstr_name) (type_params_opt:type_params_opt) (m:index) (names:names) . (clause_name "JTEok_constr_name_p") /\ (( ( type_params_opt = (TPS_nary ((MAP (\tv_ . (TP_var tv_)) tv_list))) ) ) /\ ((EVERY (\ b . b) ((MAP (\t_ . ( JTtsnamed E type_params_opt t_ 0 )) t_list)))) /\ ( ( Jlookup_EB E (name_tcn typeconstr_name) (EB_td typeconstr_name m ) )) /\ ( ( JdomE E names )) /\ ( (~MEM (name_cn constr_name) names ) ) /\ ( (LENGTH ( (t_list) ) >= 1 ) ) /\ ( ( m = LENGTH ( ((MAP (\tv_ . (TP_var tv_)) tv_list)) )) )) ==> ( ( JTEok ( (EB_pc constr_name (TPS_nary ((MAP (\tv_ . (TP_var tv_)) tv_list))) (typexprs_inj (t_list)) (TC_name typeconstr_name)) :: E ) ))) /\ ( (* JTEok_exn_constr_name_p *) !(t_list:typexpr list) (E:environment) (constr_name:constr_name) (names:names) . (clause_name "JTEok_exn_constr_name_p") /\ (((EVERY (\ b . b) ((MAP (\t_ . ( JTt E t_ 0 )) t_list)))) /\ ( ( JdomE E names )) /\ ( (~MEM (name_cn constr_name) names ) ) /\ ( (LENGTH ( (t_list) ) >= 1 ) )) ==> ( ( JTEok ( (EB_pc constr_name (TPS_nary []) (typexprs_inj (t_list)) TC_exn) :: E ) ))) /\ ( (* JTEok_record_destr *) !(field_name_list:field_name list) (tv_list:typevar list) (E:environment) (field_name:field_name) (typeconstr_name:typeconstr_name) (t:typexpr) (names:names) (m:index) . (clause_name "JTEok_record_destr") /\ (( ( JTtsnamed E (TPS_nary ((MAP (\tv_ . (TP_var tv_)) tv_list))) t 0 )) /\ ( ( JdomE E names )) /\ ( (~MEM (name_fn field_name) names ) ) /\ ( ( Jlookup_EB E (name_tcn typeconstr_name) (EB_tr typeconstr_name m (field_name_list)) )) /\ ( ( m = LENGTH ( ((MAP (\tv_ . (TP_var tv_)) tv_list)) )) ) /\ ( (MEM field_name (field_name_list) ) )) ==> ( ( JTEok ( (EB_fn field_name (TPS_nary ((MAP (\tv_ . (TP_var tv_)) tv_list))) typeconstr_name t) :: E ) ))) /\ ( (* JTEok_typeconstr_name *) !(E:environment) (typeconstr_name:typeconstr_name) (kind:kind) (names:names) . (clause_name "JTEok_typeconstr_name") /\ (( ( JTEok E )) /\ ( ( JdomE E names )) /\ ( (~MEM (name_tcn typeconstr_name) names ) )) ==> ( ( JTEok ( (EB_td typeconstr_name kind) :: E ) ))) /\ ( (* JTEok_typeconstr_eqn *) !(tv_list:typevar list) (E:environment) (typeconstr_name:typeconstr_name) (t:typexpr) (names:names) . (clause_name "JTEok_typeconstr_eqn") /\ (( ( JdomE E names )) /\ ( (~MEM (name_tcn typeconstr_name) names ) ) /\ ( ( JTtsnamed E (TPS_nary ((MAP (\tv_ . (TP_var tv_)) tv_list))) t 0 ))) ==> ( ( JTEok ( (EB_ta (TPS_nary ((MAP (\tv_ . (TP_var tv_)) tv_list))) typeconstr_name t) :: E ) ))) /\ ( (* JTEok_typeconstr_record *) !(field_name_list:field_name list) (E:environment) (typeconstr_name:typeconstr_name) (kind:kind) (names:names) . (clause_name "JTEok_typeconstr_record") /\ (( ( JTEok E )) /\ ( ( JdomE E names )) /\ ( (~MEM (name_tcn typeconstr_name) names ) ) /\ ( (ALL_DISTINCT ( ((MAP (\field_name_ . (name_fn field_name_)) field_name_list)) )) )) ==> ( ( JTEok ( (EB_tr typeconstr_name kind (field_name_list)) :: E ) ))) /\ ( (* JTEok_location *) !(E:environment) (location:location) (t:typexpr) (names:names) . (clause_name "JTEok_location") /\ (( ( JTt E t 0 )) /\ ( ( JdomE E names )) /\ ( (~MEM (name_l location) names ) )) ==> ( ( JTEok ( (EB_l location t) :: E ) ))) /\ (* defn typeconstr *) ( (* JTtypeconstr_abstract *) !(E:environment) (typeconstr_name:typeconstr_name) (kind:kind) . (clause_name "JTtypeconstr_abstract") /\ (( ( JTEok E )) /\ ( ( Jlookup_EB E (name_tcn typeconstr_name) (EB_td typeconstr_name kind) ))) ==> ( ( JTtypeconstr E (TC_name typeconstr_name) kind ))) /\ ( (* JTtypeconstr_concrete *) !(E:environment) (typeconstr_name:typeconstr_name) (kind:kind) (type_params_opt:type_params_opt) (t:typexpr) . (clause_name "JTtypeconstr_concrete") /\ (( ( JTEok E )) /\ ( ( Jlookup_EB E (name_tcn typeconstr_name) (EB_ta type_params_opt typeconstr_name t) )) /\ ( ( JTtps_kind type_params_opt kind ))) ==> ( ( JTtypeconstr E (TC_name typeconstr_name) kind ))) /\ ( (* JTtypeconstr_record *) !(field_name_list:field_name list) (E:environment) (typeconstr_name:typeconstr_name) (kind:kind) . (clause_name "JTtypeconstr_record") /\ (( ( JTEok E )) /\ ( ( Jlookup_EB E (name_tcn typeconstr_name) (EB_tr typeconstr_name kind (field_name_list)) ))) ==> ( ( JTtypeconstr E (TC_name typeconstr_name) kind ))) /\ ( (* JTtypeconstr_int *) !(E:environment) . (clause_name "JTtypeconstr_int") /\ (( ( JTEok E ))) ==> ( ( JTtypeconstr E TC_int 0 ))) /\ ( (* JTtypeconstr_char *) !(E:environment) . (clause_name "JTtypeconstr_char") /\ (( ( JTEok E ))) ==> ( ( JTtypeconstr E TC_char 0 ))) /\ ( (* JTtypeconstr_string *) !(E:environment) . (clause_name "JTtypeconstr_string") /\ (( ( JTEok E ))) ==> ( ( JTtypeconstr E TC_string 0 ))) /\ ( (* JTtypeconstr_float *) !(E:environment) . (clause_name "JTtypeconstr_float") /\ (( ( JTEok E ))) ==> ( ( JTtypeconstr E TC_float 0 ))) /\ ( (* JTtypeconstr_bool *) !(E:environment) . (clause_name "JTtypeconstr_bool") /\ (( ( JTEok E ))) ==> ( ( JTtypeconstr E TC_bool 0 ))) /\ ( (* JTtypeconstr_unit *) !(E:environment) . (clause_name "JTtypeconstr_unit") /\ (( ( JTEok E ))) ==> ( ( JTtypeconstr E TC_unit 0 ))) /\ ( (* JTtypeconstr_exn *) !(E:environment) . (clause_name "JTtypeconstr_exn") /\ (( ( JTEok E ))) ==> ( ( JTtypeconstr E TC_exn 0 ))) /\ ( (* JTtypeconstr_list *) !(E:environment) . (clause_name "JTtypeconstr_list") /\ (( ( JTEok E ))) ==> ( ( JTtypeconstr E TC_list 1 ))) /\ ( (* JTtypeconstr_option *) !(E:environment) . (clause_name "JTtypeconstr_option") /\ (( ( JTEok E ))) ==> ( ( JTtypeconstr E TC_option 1 ))) /\ ( (* JTtypeconstr_ref *) !(E:environment) . (clause_name "JTtypeconstr_ref") /\ (( ( JTEok E ))) ==> ( ( JTtypeconstr E TC_ref 1 ))) /\ (* defn ts *) ( (* JTts_forall *) !(E:environment) (t:typexpr) . (clause_name "JTts_forall") /\ (( ( JTt ( EB_tv :: E ) t 0 ))) ==> ( ( JTts E (TS_forall t) 0 ))) /\ (* defn tsnamed *) ( (* JTtsnamed_forall *) !(tv_list:typevar list) (E:environment) (t:typexpr) . (clause_name "JTtsnamed_forall") /\ (( ( JTt E (substs_typevar_typexpr ((MAP (\tv_ . (tv_, (TE_constr [] TC_unit ) )) tv_list)) t ) 0 )) /\ ( (ALL_DISTINCT ( ((MAP (\tv_ . (TP_var tv_)) tv_list)) )) )) ==> ( ( JTtsnamed E (TPS_nary ((MAP (\tv_ . (TP_var tv_)) tv_list))) t 0 ))) /\ (* defn t *) ( (* JTt_var *) !(E:environment) (idx:idx) (num:idx) . (clause_name "JTt_var") /\ (( ( JTEok E )) /\ ( ( Jidx_bound E idx ))) ==> ( ( JTt E (TE_idxvar idx num) 0 ))) /\ ( (* JTt_arrow *) !(E:environment) (t:typexpr) (t':typexpr) . (clause_name "JTt_arrow") /\ (( ( JTt E t 0 )) /\ ( ( JTt E t' 0 ))) ==> ( ( JTt E (TE_arrow t t') 0 ))) /\ ( (* JTt_tuple *) !(t_list:typexpr list) (E:environment) . (clause_name "JTt_tuple") /\ (((EVERY (\ b . b) ((MAP (\t_ . ( JTt E t_ 0 )) t_list)))) /\ ( (LENGTH ( (t_list) ) >= 2 ) )) ==> ( ( JTt E (TE_tuple (t_list)) 0 ))) /\ ( (* JTt_constr *) !(t_list:typexpr list) (E:environment) (typeconstr:typeconstr) (n:index) . (clause_name "JTt_constr") /\ (( ( JTtypeconstr E typeconstr n )) /\ ((EVERY (\ b . b) ((MAP (\t_ . ( JTt E t_ 0 )) t_list)))) /\ ( ( n = LENGTH ( (t_list) )) )) ==> ( ( JTt E (TE_constr (t_list) typeconstr) 0 ))) `; (* defns JTeq *) val (JTeq_rules, JTeq_ind, JTeq_cases) = Hol_reln ` (* defn eq *) ( (* JTeq_refl *) !(E:environment) (t:typexpr) . (clause_name "JTeq_refl") /\ (( ( JTt E t 0 ))) ==> ( ( JTeq E t t ))) /\ ( (* JTeq_sym *) !(E:environment) (t:typexpr) (t':typexpr) . (clause_name "JTeq_sym") /\ (( ( JTeq E t' t ))) ==> ( ( JTeq E t t' ))) /\ ( (* JTeq_trans *) !(E:environment) (t:typexpr) (t'':typexpr) (t':typexpr) . (clause_name "JTeq_trans") /\ (( ( JTeq E t t' )) /\ ( ( JTeq E t' t'' ))) ==> ( ( JTeq E t t'' ))) /\ ( (* JTeq_expand *) !(t_typevar_list:(typexpr#typevar) list) (E:environment) (typeconstr_name:typeconstr_name) (t:typexpr) . (clause_name "JTeq_expand") /\ (( ( JTEok E )) /\ ( ( Jlookup_EB E (name_tcn typeconstr_name) (EB_ta (TPS_nary ((MAP (\(t_,typevar_) . (TP_var typevar_)) t_typevar_list))) typeconstr_name t) )) /\ ((EVERY (\ b . b) ((MAP (\(t_,typevar_) . ( JTt E t_ 0 )) t_typevar_list))))) ==> ( ( JTeq E (TE_constr ((MAP (\(t_,typevar_) . t_) t_typevar_list)) (TC_name typeconstr_name)) (substs_typevar_typexpr ((MAP (\(t_,typevar_) . (typevar_,t_)) t_typevar_list)) t ) ))) /\ ( (* JTeq_arrow *) !(E:environment) (t1:typexpr) (t2:typexpr) (t1':typexpr) (t2':typexpr) . (clause_name "JTeq_arrow") /\ (( ( JTeq E t1 t1' )) /\ ( ( JTeq E t2 t2' ))) ==> ( ( JTeq E (TE_arrow t1 t2) (TE_arrow t1' t2') ))) /\ ( (* JTeq_tuple *) !(t_t'_list:(typexpr#typexpr) list) (E:environment) . (clause_name "JTeq_tuple") /\ (((EVERY (\ b . b) ((MAP (\(t_,t_') . ( JTeq E t_ t_' )) t_t'_list)))) /\ ( (LENGTH ( ((MAP (\(t_,t_') . t_) t_t'_list)) ) >= 2 ) )) ==> ( ( JTeq E (TE_tuple ((MAP (\(t_,t_') . t_) t_t'_list))) (TE_tuple ((MAP (\(t_,t_') . t_') t_t'_list))) ))) /\ ( (* JTeq_constr *) !(t_t'_list:(typexpr#typexpr) list) (E:environment) (typeconstr:typeconstr) (n:index) . (clause_name "JTeq_constr") /\ (( ( JTtypeconstr E typeconstr n )) /\ ((EVERY (\ b . b) ((MAP (\(t_,t_') . ( JTeq E t_ t_' )) t_t'_list)))) /\ ( ( n = LENGTH ( ((MAP (\(t_,t_') . t_) t_t'_list)) )) )) ==> ( ( JTeq E (TE_constr ((MAP (\(t_,t_') . t_) t_t'_list)) typeconstr) (TE_constr ((MAP (\(t_,t_') . t_') t_t'_list)) typeconstr) ))) `; (* defns JTidxsub *) val (JTidxsub_rules, JTidxsub_ind, JTidxsub_cases) = Hol_reln ` (* defn idxsub *) ( (* JTinxsub_alpha *) !(t_list:typexpr list) (typevar:typevar) . (clause_name "JTinxsub_alpha") ==> ( ( JTidxsub (t_list) (TE_var typevar) (TE_var typevar) ))) /\ ( (* JTinxsub_idx0 *) !(t''_list:typexpr list) (t_list:typexpr list) (t':typexpr) (num:idx) . (clause_name "JTinxsub_idx0") /\ (( ( num = LENGTH ( (t_list) )) )) ==> ( ( JTidxsub (t_list ++ [(t')] ++ t''_list) (TE_idxvar 0 num) t' ))) /\ ( (* JTinxsub_idx1 *) !(t_list:typexpr list) (num:idx) . (clause_name "JTinxsub_idx1") /\ (( (LENGTH ( (t_list) ) <= num ) )) ==> ( ( JTidxsub (t_list) (TE_idxvar 0 num) (TE_constr [] TC_unit ) ))) /\ ( (* JTinxsub_idx2 *) !(t_list:typexpr list) (idx:idx) (num:idx) . (clause_name "JTinxsub_idx2") ==> ( ( JTidxsub (t_list) (TE_idxvar ( idx + 1 ) num) (TE_idxvar idx num) ))) /\ ( (* JTinxsub_any *) !(t_list:typexpr list) . (clause_name "JTinxsub_any") ==> ( ( JTidxsub (t_list) TE_any TE_any ))) /\ ( (* JTinxsub_arrow *) !(t_list:typexpr list) (t1':typexpr) (t2':typexpr) (t1'':typexpr) (t2'':typexpr) . (clause_name "JTinxsub_arrow") /\ (( ( JTidxsub (t_list) t1' t1'' )) /\ ( ( JTidxsub (t_list) t2' t2'' ))) ==> ( ( JTidxsub (t_list) (TE_arrow t1' t2') (TE_arrow t1'' t2'') ))) /\ ( (* JTinxsub_tuple *) !(t'_t''_list:(typexpr#typexpr) list) (t_list:typexpr list) . (clause_name "JTinxsub_tuple") /\ (((EVERY (\ b . b) ((MAP (\(t_',t_'') . ( JTidxsub (t_list) t_' t_'' )) t'_t''_list))))) ==> ( ( JTidxsub (t_list) (TE_tuple ((MAP (\(t_',t_'') . t_') t'_t''_list))) (TE_tuple ((MAP (\(t_',t_'') . t_'') t'_t''_list))) ))) /\ ( (* JTinxsub_tc *) !(t'_t''_list:(typexpr#typexpr) list) (t_list:typexpr list) (typeconstr:typeconstr) . (clause_name "JTinxsub_tc") /\ (((EVERY (\ b . b) ((MAP (\(t_',t_'') . ( JTidxsub (t_list) t_' t_'' )) t'_t''_list))))) ==> ( ( JTidxsub (t_list) (TE_constr ((MAP (\(t_',t_'') . t_') t'_t''_list)) typeconstr) (TE_constr ((MAP (\(t_',t_'') . t_'') t'_t''_list)) typeconstr) ))) `; (* defns JTinst *) val (JTinst_rules, JTinst_ind, JTinst_cases) = Hol_reln ` (* defn inst *) ( (* JTinst_idx *) !(t_list:typexpr list) (E:environment) (t'':typexpr) (t':typexpr) . (clause_name "JTinst_idx") /\ (( ( JTts E (TS_forall t') 0 )) /\ ((EVERY (\ b . b) ((MAP (\t_ . ( JTt E t_ 0 )) t_list)))) /\ ( ( JTidxsub (t_list) t' t'' ))) ==> ( ( JTinst E t'' (TS_forall t') ))) `; (* defns JTinst_named *) val (JTinst_named_rules, JTinst_named_ind, JTinst_named_cases) = Hol_reln ` (* defn inst_named *) ( (* JTinst_named_named *) !(typevar_t_list:(typevar#typexpr) list) (E:environment) (t:typexpr) . (clause_name "JTinst_named_named") /\ (( ( JTtsnamed E (TPS_nary ((MAP (\(typevar_,t_) . (TP_var typevar_)) typevar_t_list))) t 0 )) /\ ((EVERY (\ b . b) ((MAP (\(typevar_,t_) . ( JTt E t_ 0 )) typevar_t_list))))) ==> ( ( JTinst_named E (substs_typevar_typexpr (typevar_t_list) t ) (TPS_nary ((MAP (\(typevar_,t_) . (TP_var typevar_)) typevar_t_list))) t ))) `; (* defns JTinst_any *) val (JTinst_any_rules, JTinst_any_ind, JTinst_any_cases) = Hol_reln ` (* defn inst_any *) ( (* JTinst_any_tyvar *) !(E:environment) (idx:idx) (num:idx) . (clause_name "JTinst_any_tyvar") /\ (( ( JTt E (TE_idxvar idx num) 0 ))) ==> ( ( JTinst_any E (TE_idxvar idx num) (TE_idxvar idx num) ))) /\ ( (* JTinst_any_any *) !(E:environment) (t:typexpr) . (clause_name "JTinst_any_any") /\ (( ( JTt E t 0 ))) ==> ( ( JTinst_any E t TE_any ))) /\ ( (* JTinst_any_arrow *) !(E:environment) (t1:typexpr) (t2:typexpr) (t1':typexpr) (t2':typexpr) . (clause_name "JTinst_any_arrow") /\ (( ( JTinst_any E t1 t1' )) /\ ( ( JTinst_any E t2 t2' ))) ==> ( ( JTinst_any E (TE_arrow t1 t2) (TE_arrow t1' t2') ))) /\ ( (* JTinst_any_tuple *) !(t_t'_list:(typexpr#typexpr) list) (E:environment) . (clause_name "JTinst_any_tuple") /\ (((EVERY (\ b . b) ((MAP (\(t_,t_') . ( JTinst_any E t_ t_' )) t_t'_list)))) /\ ( (LENGTH ( ((MAP (\(t_,t_') . t_) t_t'_list)) ) >= 2 ) )) ==> ( ( JTinst_any E (TE_tuple ((MAP (\(t_,t_') . t_) t_t'_list))) (TE_tuple ((MAP (\(t_,t_') . t_') t_t'_list))) ))) /\ ( (* JTinst_any_ctor *) !(t_t'_list:(typexpr#typexpr) list) (E:environment) (typeconstr:typeconstr) (n:index) . (clause_name "JTinst_any_ctor") /\ (((EVERY (\ b . b) ((MAP (\(t_,t_') . ( JTinst_any E t_ t_' )) t_t'_list)))) /\ ( ( JTtypeconstr E typeconstr n )) /\ ( ( n = LENGTH ( ((MAP (\(t_,t_') . t_) t_t'_list)) )) )) ==> ( ( JTinst_any E (TE_constr ((MAP (\(t_,t_') . t_) t_t'_list)) typeconstr) (TE_constr ((MAP (\(t_,t_') . t_') t_t'_list)) typeconstr) ))) `; (* defns JTval *) val (JTval_rules, JTval_ind, JTval_cases) = Hol_reln ` (* defn value_name *) ( (* JTvalue_name_value_name *) !(E:environment) (value_name:value_name) (t:typexpr) (ts:typescheme) . (clause_name "JTvalue_name_value_name") /\ (( ( Jlookup_EB E (name_vn value_name) (EB_vn value_name ts) )) /\ ( ( JTinst E t ts ))) ==> ( ( JTvalue_name E value_name t ))) `; (* defns JTfield *) val (JTfield_rules, JTfield_ind, JTfield_cases) = Hol_reln ` (* defn field *) ( (* JTfield_name *) !(t'_tv_list:(typexpr#typevar) list) (E:environment) (field_name:field_name) (typeconstr_name:typeconstr_name) (t'':typexpr) (t:typexpr) . (clause_name "JTfield_name") /\ (( ( Jlookup_EB E (name_fn field_name) (EB_fn field_name (TPS_nary ((MAP (\(t_',tv_) . (TP_var tv_)) t'_tv_list))) typeconstr_name t) )) /\ ( ( JTinst_named E (TE_arrow (TE_constr ((MAP (\(t_',tv_) . t_') t'_tv_list)) (TC_name typeconstr_name)) t'') (TPS_nary ((MAP (\(t_',tv_) . (TP_var tv_)) t'_tv_list))) (TE_arrow (TE_constr ((MAP (\(t_',tv_) . (TE_var tv_)) t'_tv_list)) (TC_name typeconstr_name)) t) ))) ==> ( ( JTfield E field_name (TE_constr ((MAP (\(t_',tv_) . t_') t'_tv_list)) (TC_name typeconstr_name)) t'' ))) `; (* defns JTconstr_p *) val (JTconstr_p_rules, JTconstr_p_ind, JTconstr_p_cases) = Hol_reln ` (* defn constr_p *) ( (* JTconstr_p_name *) !(t'_t_list:(typexpr#typexpr) list) (t''_tv_list:(typexpr#typevar) list) (E:environment) (constr_name:constr_name) (typeconstr:typeconstr) . (clause_name "JTconstr_p_name") /\ (( ( Jlookup_EB E (name_cn constr_name) (EB_pc constr_name (TPS_nary ((MAP (\(t_'',tv_) . (TP_var tv_)) t''_tv_list))) (typexprs_inj ((MAP (\(t_',t_) . t_) t'_t_list))) typeconstr) )) /\ ( ( JTinst_named E (TE_arrow (TE_tuple ((MAP (\(t_',t_) . t_') t'_t_list))) (TE_constr ((MAP (\(t_'',tv_) . t_'') t''_tv_list)) typeconstr)) (TPS_nary ((MAP (\(t_'',tv_) . (TP_var tv_)) t''_tv_list))) (TE_arrow (TE_tuple ((MAP (\(t_',t_) . t_) t'_t_list))) (TE_constr ((MAP (\(t_'',tv_) . (TE_var tv_)) t''_tv_list)) typeconstr)) ))) ==> ( ( JTconstr_p E (C_name constr_name) ((MAP (\(t_',t_) . t_') t'_t_list)) (TE_constr ((MAP (\(t_'',tv_) . t_'') t''_tv_list)) typeconstr) ))) /\ ( (* JTconstr_p_invarg *) !(E:environment) . (clause_name "JTconstr_p_invarg") /\ (( ( JTEok E ))) ==> ( ( JTconstr_p E C_invalidargument ([( (TE_constr [] TC_string ) )]) (TE_constr [] TC_exn ) ))) /\ ( (* JTconstr_p_some *) !(E:environment) (t:typexpr) . (clause_name "JTconstr_p_some") /\ (( ( JTt E t 0 ))) ==> ( ( JTconstr_p E C_some ([(t)]) (TE_constr ([ t ]) TC_option ) ))) `; (* defns JTconstr_c *) val (JTconstr_c_rules, JTconstr_c_ind, JTconstr_c_cases) = Hol_reln ` (* defn constr_c *) ( (* JTconstr_c_constr *) !(t_list:typexpr list) (E:environment) (constr_name:constr_name) (typeconstr_name:typeconstr_name) (n:index) . (clause_name "JTconstr_c_constr") /\ (( ( JTEok E )) /\ ( ( Jlookup_EB E (name_cn constr_name) (EB_cc constr_name (TC_name typeconstr_name)) )) /\ ( ( Jlookup_EB E (name_tcn typeconstr_name) (EB_td typeconstr_name n ) )) /\ ((EVERY (\ b . b) ((MAP (\t_ . ( JTt E t_ 0 )) t_list)))) /\ ( ( n = LENGTH ( (t_list) )) )) ==> ( ( JTconstr_c E (C_name constr_name) (TE_constr (t_list) (TC_name typeconstr_name)) ))) /\ ( (* JTconstr_c_exn_constr *) !(E:environment) (constr_name:constr_name) . (clause_name "JTconstr_c_exn_constr") /\ (( ( JTEok E )) /\ ( ( Jlookup_EB E (name_cn constr_name) (EB_cc constr_name TC_exn) ))) ==> ( ( JTconstr_c E (C_name constr_name) (TE_constr [] TC_exn ) ))) /\ ( (* JTconstr_c_notfound *) !(E:environment) . (clause_name "JTconstr_c_notfound") /\ (( ( JTEok E ))) ==> ( ( JTconstr_c E C_notfound (TE_constr [] TC_exn ) ))) /\ ( (* JTconstr_c_assert_fail *) !(E:environment) . (clause_name "JTconstr_c_assert_fail") /\ (( ( JTEok E ))) ==> ( ( JTconstr_c E C_assertfailure (TE_constr [] TC_exn ) ))) /\ ( (* JTconstr_c_match_fail *) !(E:environment) . (clause_name "JTconstr_c_match_fail") /\ (( ( JTEok E ))) ==> ( ( JTconstr_c E C_matchfailure (TE_constr [] TC_exn ) ))) /\ ( (* JTconstr_c_div_by_0 *) !(E:environment) . (clause_name "JTconstr_c_div_by_0") /\ (( ( JTEok E ))) ==> ( ( JTconstr_c E C_div_by_0 (TE_constr [] TC_exn ) ))) /\ ( (* JTconstr_c_none *) !(E:environment) (t:typexpr) . (clause_name "JTconstr_c_none") /\ (( ( JTt E t 0 ))) ==> ( ( JTconstr_c E C_none (TE_constr ([ t ]) TC_option ) ))) `; (* defns JTconst *) val (JTconst_rules, JTconst_ind, JTconst_cases) = Hol_reln ` (* defn const *) ( (* JTconst_int *) !(E:environment) (integer_literal:integer_literal) . (clause_name "JTconst_int") /\ (( ( JTEok E ))) ==> ( ( JTconst E (CONST_int integer_literal ) (TE_constr [] TC_int ) ))) /\ ( (* JTconst_float *) !(E:environment) (float_literal:float_literal) . (clause_name "JTconst_float") /\ (( ( JTEok E ))) ==> ( ( JTconst E (CONST_float float_literal) (TE_constr [] TC_float ) ))) /\ ( (* JTconst_char *) !(E:environment) (char_literal:char_literal) . (clause_name "JTconst_char") /\ (( ( JTEok E ))) ==> ( ( JTconst E (CONST_char char_literal) (TE_constr [] TC_char ) ))) /\ ( (* JTconst_string *) !(E:environment) (string_literal:string_literal) . (clause_name "JTconst_string") /\ (( ( JTEok E ))) ==> ( ( JTconst E (CONST_string string_literal) (TE_constr [] TC_string ) ))) /\ ( (* JTconst_constr *) !(E:environment) (constr:constr) (t:typexpr) . (clause_name "JTconst_constr") /\ (( ( JTconstr_c E constr t ))) ==> ( ( JTconst E (CONST_constr constr) t ))) /\ ( (* JTconst_false *) !(E:environment) . (clause_name "JTconst_false") /\ (( ( JTEok E ))) ==> ( ( JTconst E CONST_false (TE_constr [] TC_bool ) ))) /\ ( (* JTconst_true *) !(E:environment) . (clause_name "JTconst_true") /\ (( ( JTEok E ))) ==> ( ( JTconst E CONST_true (TE_constr [] TC_bool ) ))) /\ ( (* JTconst_unit *) !(E:environment) . (clause_name "JTconst_unit") /\ (( ( JTEok E ))) ==> ( ( JTconst E CONST_unit (TE_constr [] TC_unit ) ))) /\ ( (* JTconst_nil *) !(E:environment) (t:typexpr) . (clause_name "JTconst_nil") /\ (( ( JTt E t 0 ))) ==> ( ( JTconst E CONST_nil (TE_constr ([ t ]) TC_list ) ))) `; (* defns JTpat *) val (JTpat_rules, JTpat_ind, JTpat_cases) = Hol_reln ` (* defn pat *) ( (* JTpat_var *) !(Tsigma:Tsigma) (E:environment) (x:value_name) (t:typexpr) . (clause_name "JTpat_var") /\ (( ( JTt E t 0 ))) ==> ( ( JTpat Tsigma E (P_var x) t ( (EB_vn x (TS_forall (shiftt 0 1 t ))) :: [] ) ))) /\ ( (* JTpat_any *) !(Tsigma:Tsigma) (E:environment) (t:typexpr) . (clause_name "JTpat_any") /\ (( ( JTt E t 0 ))) ==> ( ( JTpat Tsigma E P_any t [] ))) /\ ( (* JTpat_constant *) !(Tsigma:Tsigma) (E:environment) (constant:constant) (t:typexpr) . (clause_name "JTpat_constant") /\ (( ( JTconst E constant t ))) ==> ( ( JTpat Tsigma E (P_constant constant) t [] ))) /\ ( (* JTpat_alias *) !(name_list:name list) (Tsigma:Tsigma) (E:environment) (pattern:pattern) (x:value_name) (t:typexpr) (E':environment) . (clause_name "JTpat_alias") /\ (( ( JTpat Tsigma E pattern t E' )) /\ ( ( JdomE ( (EB_vn x (TS_forall (shiftt 0 1 t ))) :: E' ) (name_list) )) /\ ( (ALL_DISTINCT ( (name_list) )) )) ==> ( ( JTpat Tsigma E (P_alias pattern x) t ( (EB_vn x (TS_forall (shiftt 0 1 t ))) :: E' ) ))) /\ ( (* JTpat_typed *) !(Tsigma:Tsigma) (E:environment) (pattern:pattern) (src_t:typexpr) (t:typexpr) (E':environment) (t':typexpr) . (clause_name "JTpat_typed") /\ ((is_src_typexpr_of_typexpr src_t) /\ ( ( JTpat Tsigma E pattern t E' )) /\ ( ( JTinst_any E t' (substs_typevar_typexpr Tsigma src_t ) )) /\ ( ( JTeq E t t' ))) ==> ( ( JTpat Tsigma E (P_typed pattern src_t) t E' ))) /\ ( (* JTpat_or *) !(Tsigma:Tsigma) (E:environment) (pattern:pattern) (pattern':pattern) (t:typexpr) (E':environment) (E'':environment) . (clause_name "JTpat_or") /\ (( ( JTpat Tsigma E pattern t E' )) /\ ( ( JTpat Tsigma E pattern' t E'' )) /\ ( (PERM ( E' ) ( E'' )) )) ==> ( ( JTpat Tsigma E (P_or pattern pattern') t E' ))) /\ ( (* JTpat_construct *) !(name_list:name list) (pattern_E_t_list:(pattern#environment#typexpr) list) (Tsigma:Tsigma) (E:environment) (constr:constr) (t:typexpr) . (clause_name "JTpat_construct") /\ (( ( JTconstr_p E constr ((MAP (\(pattern_,E_,t_) . t_) pattern_E_t_list)) t )) /\ ((EVERY (\ b . b) ((MAP (\(pattern_,E_,t_) . ( JTpat Tsigma E pattern_ t_ E_ )) pattern_E_t_list)))) /\ ( ( JdomE (FLAT (REVERSE ((MAP (\(pattern_,E_,t_) . E_) pattern_E_t_list)) )) (name_list) )) /\ ( (ALL_DISTINCT ( (name_list) )) )) ==> ( ( JTpat Tsigma E (P_construct constr ((MAP (\(pattern_,E_,t_) . pattern_) pattern_E_t_list))) t (FLAT (REVERSE ((MAP (\(pattern_,E_,t_) . E_) pattern_E_t_list)) )) ))) /\ ( (* JTpat_construct_any *) !(t_list:typexpr list) (Tsigma:Tsigma) (E:environment) (constr:constr) (t:typexpr) . (clause_name "JTpat_construct_any") /\ (( ( JTconstr_p E constr (t_list) t ))) ==> ( ( JTpat Tsigma E (P_construct_any constr) t [] ))) /\ ( (* JTpat_tuple *) !(name_list:name list) (pattern_t_E_list:(pattern#typexpr#environment) list) (Tsigma:Tsigma) (E:environment) . (clause_name "JTpat_tuple") /\ (((EVERY (\ b . b) ((MAP (\(pattern_,t_,E_) . ( JTpat Tsigma E pattern_ t_ E_ )) pattern_t_E_list)))) /\ ( (LENGTH ( ((MAP (\(pattern_,t_,E_) . pattern_) pattern_t_E_list)) ) >= 2 ) ) /\ ( ( JdomE (FLAT (REVERSE ((MAP (\(pattern_,t_,E_) . E_) pattern_t_E_list)) )) (name_list) )) /\ ( (ALL_DISTINCT ( (name_list) )) )) ==> ( ( JTpat Tsigma E (P_tuple ((MAP (\(pattern_,t_,E_) . pattern_) pattern_t_E_list))) (TE_tuple ((MAP (\(pattern_,t_,E_) . t_) pattern_t_E_list))) (FLAT (REVERSE ((MAP (\(pattern_,t_,E_) . E_) pattern_t_E_list)) )) ))) /\ ( (* JTpat_record *) !(name_list:name list) (field_name_pattern_E_t_list:(field_name#pattern#environment#typexpr) list) (Tsigma:Tsigma) (E:environment) (t:typexpr) . (clause_name "JTpat_record") /\ (((EVERY (\ b . b) ((MAP (\(field_name_,pattern_,E_,t_) . ( JTpat Tsigma E pattern_ t_ E_ )) field_name_pattern_E_t_list)))) /\ ((EVERY (\ b . b) ((MAP (\(field_name_,pattern_,E_,t_) . ( JTfield E field_name_ t t_ )) field_name_pattern_E_t_list)))) /\ ( (LENGTH ( ((MAP (\(field_name_,pattern_,E_,t_) . pattern_) field_name_pattern_E_t_list)) ) >= 1 ) ) /\ ( ( JdomE (FLAT (REVERSE ((MAP (\(field_name_,pattern_,E_,t_) . E_) field_name_pattern_E_t_list)) )) (name_list) )) /\ ( (ALL_DISTINCT ( (name_list) )) )) ==> ( ( JTpat Tsigma E (P_record ((MAP (\(field_name_,pattern_,E_,t_) . ((F_name field_name_),pattern_)) field_name_pattern_E_t_list))) t (FLAT (REVERSE ((MAP (\(field_name_,pattern_,E_,t_) . E_) field_name_pattern_E_t_list)) )) ))) /\ ( (* JTpat_cons *) !(name'_list:name list) (name_list:name list) (Tsigma:Tsigma) (E:environment) (pattern:pattern) (pattern':pattern) (t:typexpr) (E':environment) (E'':environment) . (clause_name "JTpat_cons") /\ (( ( JTpat Tsigma E pattern t E' )) /\ ( ( JTpat Tsigma E pattern' (TE_constr ([ t ]) TC_list ) E'' )) /\ ( ( JdomE E' (name_list) )) /\ ( ( JdomE E'' (name'_list) )) /\ ( (ALL_DISTINCT ( (name_list ++ name'_list) )) )) ==> ( ( JTpat Tsigma E (P_cons pattern pattern') (TE_constr ([ t ]) TC_list ) (FLAT (REVERSE ([(E')] ++ [(E'')]) )) ))) `; (* defns JTuprim *) val (JTuprim_rules, JTuprim_ind, JTuprim_cases) = Hol_reln ` (* defn uprim *) ( (* JTuprim_raise *) !(E:environment) (t:typexpr) . (clause_name "JTuprim_raise") /\ (( ( JTt E t 0 ))) ==> ( ( JTuprim E Uprim_raise (TE_arrow (TE_constr [] TC_exn ) t) ))) /\ ( (* JTuprim_not *) !(E:environment) . (clause_name "JTuprim_not") /\ (( ( JTEok E ))) ==> ( ( JTuprim E Uprim_not (TE_arrow (TE_constr [] TC_bool ) (TE_constr [] TC_bool ) ) ))) /\ ( (* JTuprim_uminus *) !(E:environment) . (clause_name "JTuprim_uminus") /\ (( ( JTEok E ))) ==> ( ( JTuprim E Uprim_minus (TE_arrow (TE_constr [] TC_int ) (TE_constr [] TC_int ) ) ))) /\ ( (* JTuprim_ref *) !(E:environment) (t:typexpr) . (clause_name "JTuprim_ref") /\ (( ( JTt E t 0 ))) ==> ( ( JTuprim E Uprim_ref (TE_arrow t (TE_constr ([ t ]) TC_ref ) ) ))) /\ ( (* JTuprim_deref *) !(E:environment) (t:typexpr) . (clause_name "JTuprim_deref") /\ (( ( JTt E t 0 ))) ==> ( ( JTuprim E Uprim_deref (TE_arrow (TE_constr ([ t ]) TC_ref ) t) ))) `; (* defns JTbprim *) val (JTbprim_rules, JTbprim_ind, JTbprim_cases) = Hol_reln ` (* defn bprim *) ( (* JTbprim_equal *) !(E:environment) (t:typexpr) . (clause_name "JTbprim_equal") /\ (( ( JTt E t 0 ))) ==> ( ( JTbprim E Bprim_equal (TE_arrow t (TE_arrow t (TE_constr [] TC_bool ) ) ) ))) /\ ( (* JTbprim_plus *) !(E:environment) . (clause_name "JTbprim_plus") /\ (( ( JTEok E ))) ==> ( ( JTbprim E Bprim_plus (TE_arrow (TE_constr [] TC_int ) (TE_arrow (TE_constr [] TC_int ) (TE_constr [] TC_int ) ) ) ))) /\ ( (* JTbprim_minus *) !(E:environment) . (clause_name "JTbprim_minus") /\ (( ( JTEok E ))) ==> ( ( JTbprim E Bprim_minus (TE_arrow (TE_constr [] TC_int ) (TE_arrow (TE_constr [] TC_int ) (TE_constr [] TC_int ) ) ) ))) /\ ( (* JTbprim_times *) !(E:environment) . (clause_name "JTbprim_times") /\ (( ( JTEok E ))) ==> ( ( JTbprim E Bprim_times (TE_arrow (TE_constr [] TC_int ) (TE_arrow (TE_constr [] TC_int ) (TE_constr [] TC_int ) ) ) ))) /\ ( (* JTbprim_div *) !(E:environment) . (clause_name "JTbprim_div") /\ (( ( JTEok E ))) ==> ( ( JTbprim E Bprim_div (TE_arrow (TE_constr [] TC_int ) (TE_arrow (TE_constr [] TC_int ) (TE_constr [] TC_int ) ) ) ))) /\ ( (* JTbprim_assign *) !(E:environment) (t:typexpr) . (clause_name "JTbprim_assign") /\ (( ( JTt E t 0 ))) ==> ( ( JTbprim E Bprim_assign (TE_arrow (TE_constr ([ t ]) TC_ref ) (TE_arrow t (TE_constr [] TC_unit ) ) ) ))) `; (* defns JTe *) val (JTe_rules, JTe_ind, JTe_cases) = Hol_reln ` (* defn e *) ( (* JTe_uprim *) !(Tsigma:Tsigma) (E:environment) (unary_prim:unary_prim) (t':typexpr) (t:typexpr) . (clause_name "JTe_uprim") /\ (( ( JTuprim E unary_prim t )) /\ ( ( JTeq E t t' ))) ==> ( ( JTe Tsigma E (Expr_uprim unary_prim) t' ))) /\ ( (* JTe_bprim *) !(Tsigma:Tsigma) (E:environment) (binary_prim:binary_prim) (t':typexpr) (t:typexpr) . (clause_name "JTe_bprim") /\ (( ( JTbprim E binary_prim t )) /\ ( ( JTeq E t t' ))) ==> ( ( JTe Tsigma E (Expr_bprim binary_prim) t' ))) /\ ( (* JTe_ident *) !(Tsigma:Tsigma) (E:environment) (value_name:value_name) (t':typexpr) (t:typexpr) . (clause_name "JTe_ident") /\ (( ( JTvalue_name E value_name t )) /\ ( ( JTeq E t t' ))) ==> ( ( JTe Tsigma E (Expr_ident value_name) t' ))) /\ ( (* JTe_constant *) !(Tsigma:Tsigma) (E:environment) (constant:constant) (t':typexpr) (t:typexpr) . (clause_name "JTe_constant") /\ (( ( JTconst E constant t )) /\ ( ( JTeq E t t' ))) ==> ( ( JTe Tsigma E (Expr_constant constant) t' ))) /\ ( (* JTe_typed *) !(Tsigma:Tsigma) (E:environment) (e:expr) (src_t:typexpr) (t:typexpr) (t':typexpr) . (clause_name "JTe_typed") /\ ((is_src_typexpr_of_typexpr src_t) /\ ( ( JTe Tsigma E e t )) /\ ( ( JTinst_any E t' (substs_typevar_typexpr Tsigma src_t ) )) /\ ( ( JTeq E t t' ))) ==> ( ( JTe Tsigma E (Expr_typed e src_t) t ))) /\ ( (* JTe_tuple *) !(e_t_list:(expr#typexpr) list) (Tsigma:Tsigma) (E:environment) (t':typexpr) . (clause_name "JTe_tuple") /\ (((EVERY (\ b . b) ((MAP (\(e_,t_) . ( JTe Tsigma E e_ t_ )) e_t_list)))) /\ ( (LENGTH ( ((MAP (\(e_,t_) . e_) e_t_list)) ) >= 2 ) ) /\ ( ( JTeq E (TE_tuple ((MAP (\(e_,t_) . t_) e_t_list))) t' ))) ==> ( ( JTe Tsigma E (Expr_tuple ((MAP (\(e_,t_) . e_) e_t_list))) t' ))) /\ ( (* JTe_construct *) !(e_t_list:(expr#typexpr) list) (Tsigma:Tsigma) (E:environment) (constr:constr) (t':typexpr) (t:typexpr) . (clause_name "JTe_construct") /\ (( ( JTconstr_p E constr ((MAP (\(e_,t_) . t_) e_t_list)) t )) /\ ((EVERY (\ b . b) ((MAP (\(e_,t_) . ( JTe Tsigma E e_ t_ )) e_t_list)))) /\ ( ( JTeq E t t' ))) ==> ( ( JTe Tsigma E (Expr_construct constr ((MAP (\(e_,t_) . e_) e_t_list))) t' ))) /\ ( (* JTe_cons *) !(Tsigma:Tsigma) (E:environment) (e1:expr) (e2:expr) (t':typexpr) (t:typexpr) . (clause_name "JTe_cons") /\ (( ( JTe Tsigma E e1 t )) /\ ( ( JTe Tsigma E e2 (TE_constr ([ t ]) TC_list ) )) /\ ( ( JTeq E (TE_constr ([ t ]) TC_list ) t' ))) ==> ( ( JTe Tsigma E (Expr_cons e1 e2) t' ))) /\ ( (* JTe_record_constr *) !(field_name'_list:field_name list) (t'_list:typexpr list) (field_name_e_t_list:(field_name#expr#typexpr) list) (Tsigma:Tsigma) (E:environment) (t':typexpr) (t:typexpr) (typeconstr_name:typeconstr_name) (kind:kind) . (clause_name "JTe_record_constr") /\ (((EVERY (\ b . b) ((MAP (\(field_name_,e_,t_) . ( JTe Tsigma E e_ t_ )) field_name_e_t_list)))) /\ ((EVERY (\ b . b) ((MAP (\(field_name_,e_,t_) . ( JTfield E field_name_ t t_ )) field_name_e_t_list)))) /\ ( ( t = (TE_constr (t'_list) (TC_name typeconstr_name)) ) ) /\ ( ( Jlookup_EB E (name_tcn typeconstr_name) (EB_tr typeconstr_name kind (field_name'_list)) )) /\ ( (PERM ( ((MAP (\(field_name_,e_,t_) . field_name_) field_name_e_t_list)) ) ( (field_name'_list) )) ) /\ ( (LENGTH ( ((MAP (\(field_name_,e_,t_) . e_) field_name_e_t_list)) ) >= 1 ) ) /\ ( ( JTeq E t t' ))) ==> ( ( JTe Tsigma E (Expr_record ((MAP (\(field_name_,e_,t_) . ((F_name field_name_),e_)) field_name_e_t_list))) t' ))) /\ ( (* JTe_record_with *) !(field_name_e_t_list:(field_name#expr#typexpr) list) (Tsigma:Tsigma) (E:environment) (expr:expr) (t':typexpr) (t:typexpr) . (clause_name "JTe_record_with") /\ (( ( JTe Tsigma E expr t )) /\ ((EVERY (\ b . b) ((MAP (\(field_name_,e_,t_) . ( JTfield E field_name_ t t_ )) field_name_e_t_list)))) /\ ((EVERY (\ b . b) ((MAP (\(field_name_,e_,t_) . ( JTe Tsigma E e_ t_ )) field_name_e_t_list)))) /\ ( (ALL_DISTINCT ( ((MAP (\(field_name_,e_,t_) . (name_fn field_name_)) field_name_e_t_list)) )) ) /\ ( (LENGTH ( ((MAP (\(field_name_,e_,t_) . e_) field_name_e_t_list)) ) >= 1 ) ) /\ ( ( JTeq E t t' ))) ==> ( ( JTe Tsigma E (Expr_override expr ((MAP (\(field_name_,e_,t_) . ((F_name field_name_),e_)) field_name_e_t_list))) t' ))) /\ ( (* JTe_apply *) !(Tsigma:Tsigma) (E:environment) (e:expr) (e1:expr) (t:typexpr) (t1:typexpr) . (clause_name "JTe_apply") /\ (( ( JTe Tsigma E e (TE_arrow t1 t) )) /\ ( ( JTe Tsigma E e1 t1 ))) ==> ( ( JTe Tsigma E (Expr_apply e e1) t ))) /\ ( (* JTe_record_proj *) !(Tsigma:Tsigma) (E:environment) (e:expr) (field_name:field_name) (t'':typexpr) (t:typexpr) (t':typexpr) . (clause_name "JTe_record_proj") /\ (( ( JTe Tsigma E e t )) /\ ( ( JTfield E field_name t t' )) /\ ( ( JTeq E t' t'' ))) ==> ( ( JTe Tsigma E (Expr_field e (F_name field_name)) t'' ))) /\ ( (* JTe_and *) !(Tsigma:Tsigma) (E:environment) (e1:expr) (e2:expr) (t:typexpr) . (clause_name "JTe_and") /\ (( ( JTe Tsigma E e1 (TE_constr [] TC_bool ) )) /\ ( ( JTe Tsigma E e2 (TE_constr [] TC_bool ) )) /\ ( ( JTeq E (TE_constr [] TC_bool ) t ))) ==> ( ( JTe Tsigma E (Expr_and e1 e2) t ))) /\ ( (* JTe_or *) !(Tsigma:Tsigma) (E:environment) (e1:expr) (e2:expr) (t:typexpr) . (clause_name "JTe_or") /\ (( ( JTe Tsigma E e1 (TE_constr [] TC_bool ) )) /\ ( ( JTe Tsigma E e2 (TE_constr [] TC_bool ) )) /\ ( ( JTeq E (TE_constr [] TC_bool ) t ))) ==> ( ( JTe Tsigma E (Expr_or e1 e2) t ))) /\ ( (* JTe_ifthenelse *) !(Tsigma:Tsigma) (E:environment) (e1:expr) (e2:expr) (e3:expr) (t:typexpr) . (clause_name "JTe_ifthenelse") /\ (( ( JTe Tsigma E e1 (TE_constr [] TC_bool ) )) /\ ( ( JTe Tsigma E e2 t )) /\ ( ( JTe Tsigma E e3 t ))) ==> ( ( JTe Tsigma E (Expr_ifthenelse e1 e2 e3) t ))) /\ ( (* JTe_while *) !(Tsigma:Tsigma) (E:environment) (e1:expr) (e2:expr) (t:typexpr) . (clause_name "JTe_while") /\ (( ( JTe Tsigma E e1 (TE_constr [] TC_bool ) )) /\ ( ( JTe Tsigma E e2 (TE_constr [] TC_unit ) )) /\ ( ( JTeq E (TE_constr [] TC_unit ) t ))) ==> ( ( JTe Tsigma E (Expr_while e1 e2) t ))) /\ ( (* JTe_for *) !(Tsigma:Tsigma) (E:environment) (lowercase_ident:lowercase_ident) (e1:expr) (for_dirn:for_dirn) (e2:expr) (e3:expr) (t:typexpr) . (clause_name "JTe_for") /\ (( ( JTe Tsigma E e1 (TE_constr [] TC_int ) )) /\ ( ( JTe Tsigma E e2 (TE_constr [] TC_int ) )) /\ ( ( JTe Tsigma ( (EB_vn (VN_id lowercase_ident) (TS_forall (shiftt 0 1 (TE_constr [] TC_int ) ))) :: E ) e3 (TE_constr [] TC_unit ) )) /\ ( ( JTeq E (TE_constr [] TC_unit ) t ))) ==> ( ( JTe Tsigma E (Expr_for (VN_id lowercase_ident) e1 for_dirn e2 e3) t ))) /\ ( (* JTe_sequence *) !(Tsigma:Tsigma) (E:environment) (e1:expr) (e2:expr) (t:typexpr) . (clause_name "JTe_sequence") /\ (( ( JTe Tsigma E e1 (TE_constr [] TC_unit ) )) /\ ( ( JTe Tsigma E e2 t ))) ==> ( ( JTe Tsigma E (Expr_sequence e1 e2) t ))) /\ ( (* JTe_match *) !(Tsigma:Tsigma) (E:environment) (e:expr) (pattern_matching:pattern_matching) (t':typexpr) (t:typexpr) . (clause_name "JTe_match") /\ (( ( JTe Tsigma E e t )) /\ ( ( JTpat_matching Tsigma E pattern_matching t t' ))) ==> ( ( JTe Tsigma E (Expr_match e pattern_matching) t' ))) /\ ( (* JTe_function *) !(Tsigma:Tsigma) (E:environment) (pattern_matching:pattern_matching) (t'':typexpr) (t:typexpr) (t':typexpr) . (clause_name "JTe_function") /\ (( ( JTpat_matching Tsigma E pattern_matching t t' )) /\ ( ( JTeq E (TE_arrow t t') t'' ))) ==> ( ( JTe Tsigma E (Expr_function pattern_matching) t'' ))) /\ ( (* JTe_try *) !(Tsigma:Tsigma) (E:environment) (e:expr) (pattern_matching:pattern_matching) (t:typexpr) . (clause_name "JTe_try") /\ (( ( JTe Tsigma E e t )) /\ ( ( JTpat_matching Tsigma E pattern_matching (TE_constr [] TC_exn ) t ))) ==> ( ( JTe Tsigma E (Expr_try e pattern_matching) t ))) /\ ( (* JTe_let_mono *) !(x_t_list:(value_name#typexpr) list) (Tsigma:Tsigma) (E:environment) (pat:pattern) (expr:expr) (e:expr) (t:typexpr) . (clause_name "JTe_let_mono") /\ (( ( JTlet_binding Tsigma E (LB_simple pat expr) (REVERSE ((MAP (\(x_,t_) . (EB_vn x_ (TS_forall (shiftt 0 1 t_ ))) ) x_t_list)) ) )) /\ ( ( JTe Tsigma (FLAT (REVERSE ([(E)] ++ [( (REVERSE ((MAP (\(x_,t_) . (EB_vn x_ (TS_forall (shiftt 0 1 t_ ))) ) x_t_list)) ) )]) )) e t ))) ==> ( ( JTe Tsigma E (Expr_let (LB_simple pat expr) e) t ))) /\ ( (* JTe_let_poly *) !(x_t_list:(value_name#typexpr) list) (Tsigma:Tsigma) (E:environment) (pat:pattern) (nexp:expr) (e:expr) (t:typexpr) . (clause_name "JTe_let_poly") /\ ((is_non_expansive_of_expr nexp) /\ ( ( JTlet_binding (shiftTsig 0 1 Tsigma ) ( EB_tv :: E ) (LB_simple pat nexp) (REVERSE ((MAP (\(x_,t_) . (EB_vn x_ (TS_forall (shiftt 0 1 t_ ))) ) x_t_list)) ) )) /\ ( ( JTe Tsigma (FLAT (REVERSE ([(E)] ++ [( (REVERSE ((MAP (\(x_,t_) . (EB_vn x_ (TS_forall t_))) x_t_list)) ) )]) )) e t ))) ==> ( ( JTe Tsigma E (Expr_let (LB_simple pat nexp) e) t ))) /\ ( (* JTe_letrec *) !(x_t_list:(value_name#typexpr) list) (Tsigma:Tsigma) (E:environment) (letrec_bindings:letrec_bindings) (e:expr) (t:typexpr) . (clause_name "JTe_letrec") /\ (( ( JTletrec_binding (shiftTsig 0 1 Tsigma ) ( EB_tv :: E ) letrec_bindings (REVERSE ((MAP (\(x_,t_) . (EB_vn x_ (TS_forall (shiftt 0 1 t_ ))) ) x_t_list)) ) )) /\ ( ( JTe Tsigma (FLAT (REVERSE ([(E)] ++ [( (REVERSE ((MAP (\(x_,t_) . (EB_vn x_ (TS_forall t_)) ) x_t_list)) ) )]) )) e t ))) ==> ( ( JTe Tsigma E (Expr_letrec letrec_bindings e) t ))) /\ ( (* JTe_assert *) !(Tsigma:Tsigma) (E:environment) (e:expr) (t:typexpr) . (clause_name "JTe_assert") /\ (( ( JTe Tsigma E e (TE_constr [] TC_bool ) )) /\ ( ( JTeq E (TE_constr [] TC_unit ) t ))) ==> ( ( JTe Tsigma E (Expr_assert e) t ))) /\ ( (* JTe_assertfalse *) !(Tsigma:Tsigma) (E:environment) (t:typexpr) . (clause_name "JTe_assertfalse") /\ (( ( JTt E t 0 ))) ==> ( ( JTe Tsigma E (Expr_assert (Expr_constant CONST_false)) t ))) /\ ( (* JTe_location *) !(Tsigma:Tsigma) (E:environment) (location:location) (t':typexpr) (t:typexpr) . (clause_name "JTe_location") /\ (( ( JTEok E )) /\ ( ( Jlookup_EB E (name_l location) (EB_l location t) )) /\ ( ( JTeq E (TE_constr ([ t ]) TC_ref ) t' ))) ==> ( ( JTe Tsigma E (Expr_location location) t' ))) /\ (* defn pat_matching *) ( (* JTpat_matching_pm *) !(pattern_e_E_list:(pattern#expr#environment) list) (Tsigma:Tsigma) (E:environment) (t:typexpr) (t':typexpr) . (clause_name "JTpat_matching_pm") /\ (((EVERY (\ b . b) ((MAP (\(pattern_,e_,E_) . ( JTpat Tsigma E pattern_ t E_ )) pattern_e_E_list)))) /\ ((EVERY (\ b . b) ((MAP (\(pattern_,e_,E_) . ( JTe Tsigma (FLAT (REVERSE ([(E)] ++ [(E_)]) )) e_ t' )) pattern_e_E_list)))) /\ ( (LENGTH ( ((MAP (\(pattern_,e_,E_) . pattern_) pattern_e_E_list)) ) >= 1 ) )) ==> ( ( JTpat_matching Tsigma E (PM_pm ((MAP (\(pattern_,e_,E_) . (PE_inj pattern_ e_)) pattern_e_E_list))) t t' ))) /\ (* defn let_binding *) ( (* JTlet_binding_poly *) !(x_t_list:(value_name#typexpr) list) (Tsigma:Tsigma) (E:environment) (pattern:pattern) (expr:expr) (t:typexpr) . (clause_name "JTlet_binding_poly") /\ (( ( JTpat Tsigma E pattern t (REVERSE ((MAP (\(x_,t_) . (EB_vn x_ (TS_forall (shiftt 0 1 t_ ))) ) x_t_list)) ) )) /\ ( ( JTe Tsigma E expr t ))) ==> ( ( JTlet_binding Tsigma E (LB_simple pattern expr) (REVERSE ((MAP (\(x_,t_) . (EB_vn x_ (TS_forall (shiftt 0 1 t_ ))) ) x_t_list)) ) ))) /\ (* defn letrec_binding *) ( (* JTletrec_binding_equal_function *) !(value_name_pattern_matching_t_t'_list:(value_name#pattern_matching#typexpr#typexpr) list) (Tsigma:Tsigma) (E:environment) (E':environment) . (clause_name "JTletrec_binding_equal_function") /\ (( ( E' = (FLAT (REVERSE ([(E)] ++ [( (REVERSE ((MAP (\(value_name_,pattern_matching_,t_,t_') . (EB_vn value_name_ (TS_forall (shiftt 0 1 (TE_arrow t_ t_') ))) ) value_name_pattern_matching_t_t'_list)) ) )]) )) ) ) /\ ((EVERY (\ b . b) ((MAP (\(value_name_,pattern_matching_,t_,t_') . ( JTpat_matching Tsigma E' pattern_matching_ t_ t_' )) value_name_pattern_matching_t_t'_list)))) /\ ( (ALL_DISTINCT ( ((MAP (\(value_name_,pattern_matching_,t_,t_') . (name_vn value_name_)) value_name_pattern_matching_t_t'_list)) )) )) ==> ( ( JTletrec_binding Tsigma E (LRBs_inj ((MAP (\(value_name_,pattern_matching_,t_,t_') . (LRB_simple value_name_ pattern_matching_)) value_name_pattern_matching_t_t'_list))) (REVERSE ((MAP (\(value_name_,pattern_matching_,t_,t_') . (EB_vn value_name_ (TS_forall (shiftt 0 1 (TE_arrow t_ t_') ))) ) value_name_pattern_matching_t_t'_list)) ) ))) `; (* defns JTconstr_decl *) val (JTconstr_decl_rules, JTconstr_decl_ind, JTconstr_decl_cases) = Hol_reln ` (* defn constr_decl *) ( (* JTconstr_decl_nullary *) !(tv_list:typevar list) (typeconstr:typeconstr) (constr_name:constr_name) . (clause_name "JTconstr_decl_nullary") ==> ( ( JTconstr_decl (TPS_nary ((MAP (\tv_ . (TP_var tv_)) tv_list))) typeconstr (CD_nullary constr_name) (EB_cc constr_name typeconstr) ))) /\ ( (* JTconstr_decl_nary *) !(tv_t_list:(typevar#typexpr) list) (typeconstr:typeconstr) (constr_name:constr_name) . (clause_name "JTconstr_decl_nary") ==> ( ( JTconstr_decl (TPS_nary ((MAP (\(tv_,t_) . (TP_var tv_)) tv_t_list))) typeconstr (CD_nary constr_name ((MAP (\(tv_,t_) . t_) tv_t_list))) (EB_pc constr_name (TPS_nary ((MAP (\(tv_,t_) . (TP_var tv_)) tv_t_list))) (typexprs_inj ((MAP (\(tv_,t_) . t_) tv_t_list))) typeconstr) ))) `; (* defns JTfield_decl *) val (JTfield_decl_rules, JTfield_decl_ind, JTfield_decl_cases) = Hol_reln ` (* defn field_decl *) ( (* JTfield_decl_only *) !(tv_list:typevar list) (typeconstr_name:typeconstr_name) (fn:field_name) (t:typexpr) . (clause_name "JTfield_decl_only") ==> ( ( JTfield_decl (TPS_nary ((MAP (\tv_ . (TP_var tv_)) tv_list))) typeconstr_name (FD_immutable fn t) (EB_fn fn (TPS_nary ((MAP (\tv_ . (TP_var tv_)) tv_list))) typeconstr_name t) ))) `; (* defns JTtypedef *) val (JTtypedef_rules, JTtypedef_ind, JTtypedef_cases) = Hol_reln ` (* defn typedef *) ( (* JTtypedef_empty *) (clause_name "JTtypedef_empty") ==> ( ( JTtypedef NIL [] [] [] ))) /\ ( (* JTtypedef_eq *) !(typedef_list:typedef list) (type_params_opt:type_params_opt) (typeconstr_name:typeconstr_name) (t:typexpr) (E:environment) (E':environment) (E'':environment) . (clause_name "JTtypedef_eq") /\ (( ( JTtypedef (typedef_list) E E' E'' ))) ==> ( ( JTtypedef ([((TD_td type_params_opt typeconstr_name (TI_eq (TE_te t))))] ++ typedef_list) E ( (EB_ta type_params_opt typeconstr_name t) :: E' ) E'' ))) /\ ( (* JTtypedef_def_sum *) !(constr_decl_EB_list:(constr_decl#environment_binding) list) (typedef_list:typedef list) (type_params_opt:type_params_opt) (typeconstr_name:typeconstr_name) (E:environment) (kind:kind) (E':environment) (E'':environment) . (clause_name "JTtypedef_def_sum") /\ (( ( JTtypedef (typedef_list) E E' E'' )) /\ ( ( JTtps_kind type_params_opt kind )) /\ ((EVERY (\ b . b) ((MAP (\(constr_decl_,EB_) . ( JTconstr_decl type_params_opt (TC_name typeconstr_name) constr_decl_ EB_ )) constr_decl_EB_list))))) ==> ( ( JTtypedef ([((TD_td type_params_opt typeconstr_name (TI_def (TR_variant ((MAP (\(constr_decl_,EB_) . constr_decl_) constr_decl_EB_list))))))] ++ typedef_list) ( (EB_td typeconstr_name kind) :: E ) E' (FLAT (REVERSE ([(E'')] ++ [( (REVERSE ((MAP (\(constr_decl_,EB_) . EB_) constr_decl_EB_list)) ) )]) )) ))) /\ ( (* JTtypedef_def_record *) !(field_name_t_EB_list:(field_name#typexpr#environment_binding) list) (typedef_list:typedef list) (type_params_opt:type_params_opt) (typeconstr_name:typeconstr_name) (E:environment) (kind:kind) (E':environment) (E'':environment) . (clause_name "JTtypedef_def_record") /\ (( ( JTtypedef (typedef_list) E E' E'' )) /\ ( ( JTtps_kind type_params_opt kind )) /\ ((EVERY (\ b . b) ((MAP (\(field_name_,t_,EB_) . ( JTfield_decl type_params_opt typeconstr_name (FD_immutable field_name_ t_) EB_ )) field_name_t_EB_list))))) ==> ( ( JTtypedef ([((TD_td type_params_opt typeconstr_name (TI_def (TR_record ((MAP (\(field_name_,t_,EB_) . (FD_immutable field_name_ t_)) field_name_t_EB_list))))))] ++ typedef_list) ( (EB_tr typeconstr_name kind ((MAP (\(field_name_,t_,EB_) . field_name_) field_name_t_EB_list))) :: E ) E' (FLAT (REVERSE ([(E'')] ++ [( (REVERSE ((MAP (\(field_name_,t_,EB_) . EB_) field_name_t_EB_list)) ) )]) )) ))) `; (* defns JTtype_definition *) val (JTtype_definition_rules, JTtype_definition_ind, JTtype_definition_cases) = Hol_reln ` (* defn type_definition *) ( (* JTtype_definition_list *) !(typedef_list:typedef list) (E:environment) (E'''':environment) (E':environment) (E'':environment) (E''':environment) . (clause_name "JTtype_definition_list") /\ (( ( JTtypedef (typedef_list) E' E'' E''' )) /\ ( ( E'''' = (FLAT (REVERSE ([(E')] ++ [(E'')] ++ [(E''')]) )) ) ) /\ ( ( JTEok (FLAT (REVERSE ([(E)] ++ [(E'''')]) )) ))) ==> ( ( JTtype_definition E (TDF_tdf (typedef_list)) E'''' ))) /\ ( (* JTtype_definition_swap *) !(typedef''_list:typedef list) (typedef_list:typedef list) (E:environment) (typedef:typedef) (typedef':typedef) (E':environment) . (clause_name "JTtype_definition_swap") /\ (( ( JTtype_definition E (TDF_tdf (typedef_list ++ [(typedef')] ++ [(typedef)] ++ typedef''_list)) E' ))) ==> ( ( JTtype_definition E (TDF_tdf (typedef_list ++ [(typedef)] ++ [(typedef')] ++ typedef''_list)) E' ))) `; (* defns JTdefinition *) val (JTdefinition_rules, JTdefinition_ind, JTdefinition_cases) = Hol_reln ` (* defn definition *) ( (* JTdefinition_let_poly *) !(x_t'_list:(value_name#typexpr) list) (E:environment) (pat:pattern) (nexp:expr) (Tsigma:Tsigma) . (clause_name "JTdefinition_let_poly") /\ ((is_non_expansive_of_expr nexp) /\ ( ( JTlet_binding Tsigma ( EB_tv :: E ) (LB_simple pat nexp) (REVERSE ((MAP (\(x_,t_') . (EB_vn x_ (TS_forall (shiftt 0 1 t_' ))) ) x_t'_list)) ) ))) ==> ( ( JTdefinition E (D_let (LB_simple pat nexp)) (REVERSE ((MAP (\(x_,t_') . (EB_vn x_ (TS_forall t_')) ) x_t'_list)) ) ))) /\ ( (* JTdefinition_let_mono *) !(x_t'_list:(value_name#typexpr) list) (E:environment) (pat:pattern) (expr:expr) (Tsigma:Tsigma) . (clause_name "JTdefinition_let_mono") /\ (( ( JTlet_binding Tsigma E (LB_simple pat expr) (REVERSE ((MAP (\(x_,t_') . (EB_vn x_ (TS_forall (shiftt 0 1 t_' ))) ) x_t'_list)) ) ))) ==> ( ( JTdefinition E (D_let (LB_simple pat expr)) (REVERSE ((MAP (\(x_,t_') . (EB_vn x_ (TS_forall (shiftt 0 1 t_' ))) ) x_t'_list)) ) ))) /\ ( (* JTdefinition_letrec *) !(x_t'_list:(value_name#typexpr) list) (E:environment) (letrec_bindings:letrec_bindings) (Tsigma:Tsigma) . (clause_name "JTdefinition_letrec") /\ (( ( JTletrec_binding Tsigma ( EB_tv :: E ) letrec_bindings (REVERSE ((MAP (\(x_,t_') . (EB_vn x_ (TS_forall (shiftt 0 1 t_' ))) ) x_t'_list)) ) ))) ==> ( ( JTdefinition E (D_letrec letrec_bindings) (REVERSE ((MAP (\(x_,t_') . (EB_vn x_ (TS_forall t_')) ) x_t'_list)) ) ))) /\ ( (* JTdefinition_typedef *) !(typedef_list:typedef list) (E:environment) (E':environment) . (clause_name "JTdefinition_typedef") /\ (( ( JTtype_definition E (TDF_tdf (typedef_list)) E' ))) ==> ( ( JTdefinition E (D_type (TDF_tdf (typedef_list))) E' ))) /\ ( (* JTdefinition_exndef *) !(E:environment) (constr_decl:constr_decl) (EB:environment_binding) . (clause_name "JTdefinition_exndef") /\ (( ( JTEok E )) /\ ( ( JTconstr_decl (TPS_nary []) TC_exn constr_decl EB ))) ==> ( ( JTdefinition E (D_exception (ED_def constr_decl)) (REVERSE ([(EB)]) ) ))) `; (* defns JTdefinitions *) val (JTdefinitions_rules, JTdefinitions_ind, JTdefinitions_cases) = Hol_reln ` (* defn definitions *) ( (* JTdefinitions_empty *) !(E:environment) . (clause_name "JTdefinitions_empty") /\ (( ( JTEok E ))) ==> ( ( JTdefinitions E Ds_nil (REVERSE NIL ) ))) /\ ( (* JTdefinitions_item *) !(E:environment) (definition:definition) (definitions':definitions) (E':environment) (E'':environment) . (clause_name "JTdefinitions_item") /\ (( ( JTdefinition E definition E' )) /\ ( ( JTdefinitions (FLAT (REVERSE ([(E)] ++ [(E')]) )) definitions' E'' ))) ==> ( ( JTdefinitions E (Ds_cons definition definitions') (FLAT (REVERSE ([(E')] ++ [(E'')]) )) ))) `; (* defns JTprog *) val (JTprog_rules, JTprog_ind, JTprog_cases) = Hol_reln ` (* defn prog *) ( (* JTprog_defs *) !(E:environment) (definitions:definitions) (E':environment) . (clause_name "JTprog_defs") /\ (( ( JTdefinitions E definitions E' ))) ==> ( ( JTprog E (Prog_defs definitions) E' ))) /\ ( (* JTprog_raise *) !(E:environment) (v:expr) (Tsigma:Tsigma) (t:typexpr) . (clause_name "JTprog_raise") /\ ((is_value_of_expr v) /\ ( ( JTe Tsigma E v t ))) ==> ( ( JTprog E (Prog_raise v) (REVERSE NIL ) ))) `; (* defns JTstore *) val (JTstore_rules, JTstore_ind, JTstore_cases) = Hol_reln ` (* defn store *) ( (* JTstore_empty *) !(E:environment) . (clause_name "JTstore_empty") ==> ( ( JTstore E [] (REVERSE NIL ) ))) /\ ( (* JTstore_map *) !(E:environment) (store:store) (l:index) (v:expr) (E':environment) (t:typexpr) . (clause_name "JTstore_map") /\ ((is_value_of_expr v) /\ ( ( JTstore E store E' )) /\ ( ( JTe NIL E v t ))) ==> ( ( JTstore E (( l , v ):: store ) ( (EB_l l t) :: E' ) ))) `; (* defns JTtop *) val (JTtop_rules, JTtop_ind, JTtop_cases) = Hol_reln ` (* defn top *) ( (* JTtop_defs *) !(E:environment) (program:program) (store:store) (E':environment) (E'':environment) . (clause_name "JTtop_defs") /\ (( ( JTstore (FLAT (REVERSE ([(E)] ++ [(E')]) )) store E' )) /\ ( ( JTprog (FLAT (REVERSE ([(E)] ++ [(E')]) )) program E'' ))) ==> ( ( JTtop E program store (FLAT (REVERSE ([(E')] ++ [(E'')]) )) ))) `; (* defns JTLin *) val (JTLin_rules, JTLin_ind, JTLin_cases) = Hol_reln ` (* defn Lin *) ( (* JTLin_nil *) !(Tsigma:Tsigma) (E:environment) . (clause_name "JTLin_nil") ==> ( ( JTLin Tsigma E Lab_nil ))) /\ ( (* JTLin_alloc *) !(Tsigma:Tsigma) (E:environment) (v:expr) (location:location) (names:names) . (clause_name "JTLin_alloc") /\ (( ( JdomE E names )) /\ ( (~MEM (name_l location) names ) )) ==> ( ( JTLin Tsigma E (Lab_alloc v location) ))) /\ ( (* JTLin_deref *) !(Tsigma:Tsigma) (E:environment) (location:location) (v:expr) (t:typexpr) . (clause_name "JTLin_deref") /\ ((is_value_of_expr v) /\ ( ( JTe Tsigma E v t )) /\ ( ( Jlookup_EB E (name_l location) (EB_l location t) ))) ==> ( ( JTLin Tsigma E (Lab_deref location v) ))) /\ ( (* JTLin_assign *) !(Tsigma:Tsigma) (E:environment) (location:location) (v:expr) . (clause_name "JTLin_assign") ==> ( ( JTLin Tsigma E (Lab_assign location v) ))) `; (* defns JTLout *) val (JTLout_rules, JTLout_ind, JTLout_cases) = Hol_reln ` (* defn Lout *) ( (* JTLout_nil *) !(Tsigma:Tsigma) (E:environment) . (clause_name "JTLout_nil") ==> ( ( JTLout Tsigma E Lab_nil (REVERSE NIL ) ))) /\ ( (* JTLout_alloc *) !(Tsigma:Tsigma) (E:environment) (location:location) (t:typexpr) (v:expr) . (clause_name "JTLout_alloc") /\ ((is_value_of_expr v) /\ ( ( JTe Tsigma E v t ))) ==> ( ( JTLout Tsigma E (Lab_alloc v location) (REVERSE ([( (EB_l location t) )]) ) ))) /\ ( (* JTLout_deref *) !(Tsigma:Tsigma) (E:environment) (location:location) (v:expr) . (clause_name "JTLout_deref") ==> ( ( JTLout Tsigma E (Lab_deref location v) (REVERSE NIL ) ))) /\ ( (* JTLout_assign *) !(Tsigma:Tsigma) (E:environment) (location:location) (v:expr) (t:typexpr) . (clause_name "JTLout_assign") /\ ((is_value_of_expr v) /\ ( ( JTe Tsigma E v t )) /\ ( ( Jlookup_EB E (name_l location) (EB_l location t) ))) ==> ( ( JTLout Tsigma E (Lab_assign location v) (REVERSE NIL ) ))) `; (* defns JmatchP *) val (JmatchP_rules, JmatchP_ind, JmatchP_cases) = Hol_reln ` (* defn matchP *) ( (* JM_matchP_var *) !(v:expr) (x:value_name) . (clause_name "JM_matchP_var") /\ ((is_value_of_expr v)) ==> ( ( JM_matchP v (P_var x) ))) /\ ( (* JM_matchP_any *) !(v:expr) . (clause_name "JM_matchP_any") /\ ((is_value_of_expr v)) ==> ( ( JM_matchP v P_any ))) /\ ( (* JM_matchP_constant *) !(constant:constant) . (clause_name "JM_matchP_constant") ==> ( ( JM_matchP (Expr_constant constant) (P_constant constant) ))) /\ ( (* JM_matchP_alias *) !(v:expr) (pat:pattern) (x:value_name) . (clause_name "JM_matchP_alias") /\ ((is_value_of_expr v) /\ ( ( JM_matchP v pat ))) ==> ( ( JM_matchP v (P_alias pat x) ))) /\ ( (* JM_matchP_typed *) !(v:expr) (pat:pattern) (t:typexpr) . (clause_name "JM_matchP_typed") /\ ((is_value_of_expr v) /\ ( ( JM_matchP v pat ))) ==> ( ( JM_matchP v (P_typed pat t) ))) /\ ( (* JM_matchP_or_left *) !(v:expr) (pat1:pattern) (pat2:pattern) . (clause_name "JM_matchP_or_left") /\ ((is_value_of_expr v) /\ ( ( JM_matchP v pat1 ))) ==> ( ( JM_matchP v (P_or pat1 pat2) ))) /\ ( (* JM_matchP_or_right *) !(v:expr) (pat1:pattern) (pat2:pattern) . (clause_name "JM_matchP_or_right") /\ ((is_value_of_expr v) /\ ( ( JM_matchP v pat2 ))) ==> ( ( JM_matchP v (P_or pat1 pat2) ))) /\ ( (* JM_matchP_construct *) !(v_pat_list:(expr#pattern) list) (constr:constr) . (clause_name "JM_matchP_construct") /\ ((EVERY (\(v_,pat_). is_value_of_expr v_) v_pat_list) /\ ((EVERY (\ b . b) ((MAP (\(v_,pat_) . ( JM_matchP v_ pat_ )) v_pat_list))))) ==> ( ( JM_matchP (Expr_construct constr ((MAP (\(v_,pat_) . v_) v_pat_list))) (P_construct constr ((MAP (\(v_,pat_) . pat_) v_pat_list))) ))) /\ ( (* JM_matchP_construct_any *) !(v_list:expr list) (constr:constr) . (clause_name "JM_matchP_construct_any") /\ ((EVERY (\v_. is_value_of_expr v_) v_list)) ==> ( ( JM_matchP (Expr_construct constr (v_list)) (P_construct_any constr) ))) /\ ( (* JM_matchP_tuple *) !(v_pat_list:(expr#pattern) list) . (clause_name "JM_matchP_tuple") /\ ((EVERY (\(v_,pat_). is_value_of_expr v_) v_pat_list) /\ ((EVERY (\ b . b) ((MAP (\(v_,pat_) . ( JM_matchP v_ pat_ )) v_pat_list))))) ==> ( ( JM_matchP (Expr_tuple ((MAP (\(v_,pat_) . v_) v_pat_list))) (P_tuple ((MAP (\(v_,pat_) . pat_) v_pat_list))) ))) /\ ( (* JM_matchP_record *) !(fn_v''_list:(field_name#expr) list) (field_name'_pat_v'_list:(field_name#pattern#expr) list) (field_name_v_list:(field_name#expr) list) . (clause_name "JM_matchP_record") /\ ((EVERY (\(fn_,v_''). is_value_of_expr v_'') fn_v''_list) /\ (EVERY (\(field_name_',pat_,v_'). is_value_of_expr v_') field_name'_pat_v'_list) /\ (EVERY (\(field_name_,v_). is_value_of_expr v_) field_name_v_list) /\ ( (PERM ( ((MAP (\(field_name_',pat_,v_') . (field_name_',v_')) field_name'_pat_v'_list) ++ fn_v''_list) ) ( (field_name_v_list) )) ) /\ ((EVERY (\ b . b) ((MAP (\(field_name_',pat_,v_') . ( JM_matchP v_' pat_ )) field_name'_pat_v'_list)))) /\ ( (ALL_DISTINCT ( ((MAP (\(field_name_,v_) . (name_fn field_name_)) field_name_v_list)) )) )) ==> ( ( JM_matchP (Expr_record ((MAP (\(field_name_,v_) . ((F_name field_name_),v_)) field_name_v_list))) (P_record ((MAP (\(field_name_',pat_,v_') . ((F_name field_name_'),pat_)) field_name'_pat_v'_list))) ))) /\ ( (* JM_matchP_cons *) !(v1:expr) (v2:expr) (pat1:pattern) (pat2:pattern) . (clause_name "JM_matchP_cons") /\ ((is_value_of_expr v1) /\ (is_value_of_expr v2) /\ ( ( JM_matchP v1 pat1 )) /\ ( ( JM_matchP v2 pat2 ))) ==> ( ( JM_matchP (Expr_cons v1 v2) (P_cons pat1 pat2) ))) `; (* defns Jmatch *) val (Jmatch_rules, Jmatch_ind, Jmatch_cases) = Hol_reln ` (* defn match *) ( (* JM_match_var *) !(v:expr) (x:value_name) . (clause_name "JM_match_var") /\ ((is_value_of_expr v)) ==> ( ( JM_match v (P_var x) (substs_x_xs ([(x,v)])) ))) /\ ( (* JM_match_any *) !(v:expr) . (clause_name "JM_match_any") /\ ((is_value_of_expr v)) ==> ( ( JM_match v P_any (substs_x_xs NIL) ))) /\ ( (* JM_match_constant *) !(constant:constant) . (clause_name "JM_match_constant") ==> ( ( JM_match (Expr_constant constant) (P_constant constant) (substs_x_xs NIL) ))) /\ ( (* JM_match_alias *) !(x_v_list:(value_name#expr) list) (v:expr) (pat:pattern) (x:value_name) . (clause_name "JM_match_alias") /\ ((is_value_of_expr v) /\ (EVERY (\(x_,v_). is_value_of_expr v_) x_v_list) /\ ( ( JM_match v pat (substs_x_xs (x_v_list)) ))) ==> ( ( JM_match v (P_alias pat x) (substs_x_xs (x_v_list ++ [(x,v)])) ))) /\ ( (* JM_match_typed *) !(x_v_list:(value_name#expr) list) (v:expr) (pat:pattern) (t:typexpr) . (clause_name "JM_match_typed") /\ ((is_value_of_expr v) /\ (EVERY (\(x_,v_). is_value_of_expr v_) x_v_list) /\ ( ( JM_match v pat (substs_x_xs (x_v_list)) ))) ==> ( ( JM_match v (P_typed pat t) (substs_x_xs (x_v_list)) ))) /\ ( (* JM_match_or_left *) !(x_v_list:(value_name#expr) list) (v:expr) (pat1:pattern) (pat2:pattern) . (clause_name "JM_match_or_left") /\ ((is_value_of_expr v) /\ (EVERY (\(x_,v_). is_value_of_expr v_) x_v_list) /\ ( ( JM_match v pat1 (substs_x_xs (x_v_list)) ))) ==> ( ( JM_match v (P_or pat1 pat2) (substs_x_xs (x_v_list)) ))) /\ ( (* JM_match_or_right *) !(x_v_list:(value_name#expr) list) (pat1:pattern) (pat2:pattern) (v:expr) . (clause_name "JM_match_or_right") /\ ((is_value_of_expr v) /\ (EVERY (\(x_,v_). is_value_of_expr v_) x_v_list) /\ ( (~JM_matchP v pat1 ) ) /\ ( ( JM_match v pat2 (substs_x_xs (x_v_list)) ))) ==> ( ( JM_match v (P_or pat1 pat2) (substs_x_xs (x_v_list)) ))) /\ ( (* JM_match_construct *) !(v_pat_substs_x_list:(expr#pattern#substs_x) list) (constr:constr) . (clause_name "JM_match_construct") /\ ((EVERY (\(v_,pat_,substs_x_). is_value_of_expr v_) v_pat_substs_x_list) /\ ((EVERY (\ b . b) ((MAP (\(v_,pat_,substs_x_) . ( JM_match v_ pat_ substs_x_ )) v_pat_substs_x_list))))) ==> ( ( JM_match (Expr_construct constr ((MAP (\(v_,pat_,substs_x_) . v_) v_pat_substs_x_list))) (P_construct constr ((MAP (\(v_,pat_,substs_x_) . pat_) v_pat_substs_x_list))) (substs_x_xs (FLAT (MAP (\x. case x of substs_x_xs l -> l) ((MAP (\(v_,pat_,substs_x_) . substs_x_) v_pat_substs_x_list)) ))) ))) /\ ( (* JM_match_construct_any *) !(v_list:expr list) (constr:constr) . (clause_name "JM_match_construct_any") /\ ((EVERY (\v_. is_value_of_expr v_) v_list)) ==> ( ( JM_match (Expr_construct constr (v_list)) (P_construct_any constr) (substs_x_xs NIL) ))) /\ ( (* JM_match_tuple *) !(v_pat_substs_x_list:(expr#pattern#substs_x) list) . (clause_name "JM_match_tuple") /\ ((EVERY (\(v_,pat_,substs_x_). is_value_of_expr v_) v_pat_substs_x_list) /\ ((EVERY (\ b . b) ((MAP (\(v_,pat_,substs_x_) . ( JM_match v_ pat_ substs_x_ )) v_pat_substs_x_list))))) ==> ( ( JM_match (Expr_tuple ((MAP (\(v_,pat_,substs_x_) . v_) v_pat_substs_x_list))) (P_tuple ((MAP (\(v_,pat_,substs_x_) . pat_) v_pat_substs_x_list))) (substs_x_xs (FLAT (MAP (\x. case x of substs_x_xs l -> l) ((MAP (\(v_,pat_,substs_x_) . substs_x_) v_pat_substs_x_list)) ))) ))) /\ ( (* JM_match_record *) !(fn_v''_list:(field_name#expr) list) (field_name'_pat_substs_x_v'_list:(field_name#pattern#substs_x#expr) list) (field_name_v_list:(field_name#expr) list) . (clause_name "JM_match_record") /\ ((EVERY (\(fn_,v_''). is_value_of_expr v_'') fn_v''_list) /\ (EVERY (\(field_name_',pat_,substs_x_,v_'). is_value_of_expr v_') field_name'_pat_substs_x_v'_list) /\ (EVERY (\(field_name_,v_). is_value_of_expr v_) field_name_v_list) /\ ( (PERM ( ((MAP (\(field_name_',pat_,substs_x_,v_') . (field_name_',v_')) field_name'_pat_substs_x_v'_list) ++ fn_v''_list) ) ( (field_name_v_list) )) ) /\ ((EVERY (\ b . b) ((MAP (\(field_name_',pat_,substs_x_,v_') . ( JM_match v_' pat_ substs_x_ )) field_name'_pat_substs_x_v'_list)))) /\ ( (ALL_DISTINCT ( ((MAP (\(field_name_,v_) . (name_fn field_name_)) field_name_v_list)) )) )) ==> ( ( JM_match (Expr_record ((MAP (\(field_name_,v_) . ((F_name field_name_),v_)) field_name_v_list))) (P_record ((MAP (\(field_name_',pat_,substs_x_,v_') . ((F_name field_name_'),pat_)) field_name'_pat_substs_x_v'_list))) (substs_x_xs (FLAT (MAP (\x. case x of substs_x_xs l -> l) ((MAP (\(field_name_',pat_,substs_x_,v_') . substs_x_) field_name'_pat_substs_x_v'_list)) ))) ))) /\ ( (* JM_match_cons *) !(v1:expr) (v2:expr) (pat1:pattern) (pat2:pattern) (substs_x1:substs_x) (substs_x2:substs_x) . (clause_name "JM_match_cons") /\ ((is_value_of_expr v1) /\ (is_value_of_expr v2) /\ ( ( JM_match v1 pat1 substs_x1 )) /\ ( ( JM_match v2 pat2 substs_x2 ))) ==> ( ( JM_match (Expr_cons v1 v2) (P_cons pat1 pat2) (substs_x_xs (FLAT (MAP (\x. case x of substs_x_xs l -> l) ([(substs_x1)] ++ [(substs_x2)]) ))) ))) `; (* defns Jrecfun *) val (Jrecfun_rules, Jrecfun_ind, Jrecfun_cases) = Hol_reln ` (* defn recfun *) ( (* Jrecfun_letrec *) !(x_pattern_matching_list:(value_name#pattern_matching) list) (letrec_bindings:letrec_bindings) (pattern_matching:pattern_matching) . (clause_name "Jrecfun_letrec") /\ (( ( letrec_bindings = (LRBs_inj ((MAP (\(x_,pattern_matching_) . (LRB_simple x_ pattern_matching_)) x_pattern_matching_list))) ) )) ==> ( ( Jrecfun letrec_bindings pattern_matching (substs_value_name_expr (case (substs_x_xs ((MAP (\(x_,pattern_matching_) . (x_,(Expr_letrec letrec_bindings (Expr_ident x_)))) x_pattern_matching_list))) of substs_x_xs l -> l) (Expr_function pattern_matching) ) ))) `; (* defns Jfunval *) val (Jfunval_rules, Jfunval_ind, Jfunval_cases) = Hol_reln ` (* defn funval *) ( (* Jfunval_up *) !(unary_prim:unary_prim) . (clause_name "Jfunval_up") ==> ( ( Jfunval (Expr_uprim unary_prim) ))) /\ ( (* Jfunval_bp *) !(binary_prim:binary_prim) . (clause_name "Jfunval_bp") ==> ( ( Jfunval (Expr_bprim binary_prim) ))) /\ ( (* Jfunval_bp_app *) !(binary_prim:binary_prim) (v:expr) . (clause_name "Jfunval_bp_app") /\ ((is_value_of_expr v)) ==> ( ( Jfunval (Expr_apply (Expr_bprim binary_prim) v) ))) /\ ( (* Jfunval_func *) !(pattern_matching:pattern_matching) . (clause_name "Jfunval_func") ==> ( ( Jfunval (Expr_function pattern_matching) ))) `; (* defns JRuprim *) val (JRuprim_rules, JRuprim_ind, JRuprim_cases) = Hol_reln ` (* defn Ruprim *) ( (* Juprim_not_true *) (clause_name "Juprim_not_true") ==> ( ( JRuprim Uprim_not (Expr_constant CONST_true) Lab_nil (Expr_constant CONST_false) ))) /\ ( (* Juprim_not_false *) (clause_name "Juprim_not_false") ==> ( ( JRuprim Uprim_not (Expr_constant CONST_false) Lab_nil (Expr_constant CONST_true) ))) /\ ( (* Juprim_uminus *) !(intn:intn) . (clause_name "Juprim_uminus") ==> ( ( JRuprim Uprim_minus (Expr_constant (CONST_int intn)) Lab_nil (Expr_constant (CONST_int ( 0w - intn ) )) ))) /\ ( (* Juprim_ref_alloc *) !(v:expr) (l:index) . (clause_name "Juprim_ref_alloc") /\ ((is_value_of_expr v)) ==> ( ( JRuprim Uprim_ref v (Lab_alloc v l) (Expr_location l) ))) /\ ( (* Juprim_deref *) !(l:index) (v:expr) . (clause_name "Juprim_deref") /\ ((is_value_of_expr v)) ==> ( ( JRuprim Uprim_deref (Expr_location l) (Lab_deref l v) v ))) `; (* defns JRbprim *) val (JRbprim_rules, JRbprim_ind, JRbprim_cases) = Hol_reln ` (* defn Rbprim *) ( (* Jbprim_equal_fun *) !(v:expr) (v':expr) . (clause_name "Jbprim_equal_fun") /\ ((is_value_of_expr v) /\ (is_value_of_expr v') /\ ( ( Jfunval v ))) ==> ( ( JRbprim v Bprim_equal v' Lab_nil (Expr_apply (Expr_uprim Uprim_raise) (Expr_construct C_invalidargument ([((Expr_constant (CONST_string "equal: functional value") ))])) ) ))) /\ ( (* Jbprim_equal_const_true *) !(constant:constant) . (clause_name "Jbprim_equal_const_true") ==> ( ( JRbprim (Expr_constant constant) Bprim_equal (Expr_constant constant) Lab_nil (Expr_constant CONST_true) ))) /\ ( (* Jbprim_equal_const_false *) !(constant:constant) (constant':constant) . (clause_name "Jbprim_equal_const_false") /\ (( (~( constant = constant' )) )) ==> ( ( JRbprim (Expr_constant constant) Bprim_equal (Expr_constant constant') Lab_nil (Expr_constant CONST_false) ))) /\ ( (* Jbprim_equal_loc *) !(l:index) (l':index) . (clause_name "Jbprim_equal_loc") ==> ( ( JRbprim (Expr_location l) Bprim_equal (Expr_location l') Lab_nil (Expr_apply (Expr_apply (Expr_bprim Bprim_equal) (Expr_apply (Expr_uprim Uprim_deref) (Expr_location l)) ) (Expr_apply (Expr_uprim Uprim_deref) (Expr_location l')) ) ))) /\ ( (* Jbprim_equal_cons *) !(v1:expr) (v2:expr) (v1':expr) (v2':expr) . (clause_name "Jbprim_equal_cons") /\ ((is_value_of_expr v1) /\ (is_value_of_expr v2) /\ (is_value_of_expr v1') /\ (is_value_of_expr v2')) ==> ( ( JRbprim (Expr_cons v1 v2) Bprim_equal (Expr_cons v1' v2') Lab_nil (Expr_and (Expr_apply (Expr_apply (Expr_bprim Bprim_equal) v1) v1') (Expr_apply (Expr_apply (Expr_bprim Bprim_equal) v2) v2') ) ))) /\ ( (* Jbprim_equal_cons_nil *) !(v1:expr) (v2:expr) . (clause_name "Jbprim_equal_cons_nil") /\ ((is_value_of_expr v1) /\ (is_value_of_expr v2)) ==> ( ( JRbprim (Expr_cons v1 v2) Bprim_equal (Expr_constant CONST_nil) Lab_nil (Expr_constant CONST_false) ))) /\ ( (* Jbprim_equal_nil_cons *) !(v1:expr) (v2:expr) . (clause_name "Jbprim_equal_nil_cons") /\ ((is_value_of_expr v1) /\ (is_value_of_expr v2)) ==> ( ( JRbprim (Expr_constant CONST_nil) Bprim_equal (Expr_cons v1 v2) Lab_nil (Expr_constant CONST_false) ))) /\ ( (* Jbprim_equal_tuple *) !(v_v'_list:(expr#expr) list) . (clause_name "Jbprim_equal_tuple") /\ ((EVERY (\(v_,v_'). is_value_of_expr v_) v_v'_list) /\ (EVERY (\(v_,v_'). is_value_of_expr v_') v_v'_list) /\ ( (LENGTH ( ((MAP (\(v_,v_') . v_) v_v'_list)) ) >= 2 ) )) ==> ( ( JRbprim (Expr_tuple ((MAP (\(v_,v_') . v_) v_v'_list))) Bprim_equal (Expr_tuple ((MAP (\(v_,v_') . v_') v_v'_list))) Lab_nil (FOLDR Expr_and (Expr_constant CONST_true) ((MAP (\(v_,v_') . (Expr_apply (Expr_apply (Expr_bprim Bprim_equal) v_) v_')) v_v'_list)) ) ))) /\ ( (* Jbprim_equal_constr *) !(v_v'_list:(expr#expr) list) (constr:constr) . (clause_name "Jbprim_equal_constr") /\ ((EVERY (\(v_,v_'). is_value_of_expr v_) v_v'_list) /\ (EVERY (\(v_,v_'). is_value_of_expr v_') v_v'_list)) ==> ( ( JRbprim (Expr_construct constr ((MAP (\(v_,v_') . v_) v_v'_list))) Bprim_equal (Expr_construct constr ((MAP (\(v_,v_') . v_') v_v'_list))) Lab_nil (FOLDR Expr_and (Expr_constant CONST_true) ((MAP (\(v_,v_') . (Expr_apply (Expr_apply (Expr_bprim Bprim_equal) v_) v_')) v_v'_list)) ) ))) /\ ( (* Jbprim_equal_constr_false *) !(v'_list:expr list) (v_list:expr list) (constr:constr) (constr':constr) . (clause_name "Jbprim_equal_constr_false") /\ ((EVERY (\v_'. is_value_of_expr v_') v'_list) /\ (EVERY (\v_. is_value_of_expr v_) v_list) /\ ( (~( (CONST_constr constr) = (CONST_constr constr') )) )) ==> ( ( JRbprim (Expr_construct constr (v_list)) Bprim_equal (Expr_construct constr' (v'_list)) Lab_nil (Expr_constant CONST_false) ))) /\ ( (* Jbprim_equal_const_constr_false *) !(v_list:expr list) (constr':constr) (constr:constr) . (clause_name "Jbprim_equal_const_constr_false") /\ ((EVERY (\v_. is_value_of_expr v_) v_list)) ==> ( ( JRbprim (Expr_constant (CONST_constr constr')) Bprim_equal (Expr_construct constr (v_list)) Lab_nil (Expr_constant CONST_false) ))) /\ ( (* Jbprim_equal_constr_const_false *) !(v_list:expr list) (constr:constr) (constr':constr) . (clause_name "Jbprim_equal_constr_const_false") /\ ((EVERY (\v_. is_value_of_expr v_) v_list)) ==> ( ( JRbprim (Expr_construct constr (v_list)) Bprim_equal (Expr_constant (CONST_constr constr')) Lab_nil (Expr_constant CONST_false) ))) /\ ( (* Jbprim_equal_rec *) !(fn''_v''_list:(field_name#expr) list) (fn_v_list:(field_name#expr) list) (v':expr) . (clause_name "Jbprim_equal_rec") /\ ((is_value_of_expr v') /\ (EVERY (\(fn_'',v_''). is_value_of_expr v_'') fn''_v''_list) /\ (EVERY (\(fn_,v_). is_value_of_expr v_) fn_v_list) /\ ( ( v' = (Expr_record ((MAP (\(fn_'',v_'') . ((F_name fn_''),v_'')) fn''_v''_list))) ) ) /\ ( (PERM ( ((MAP (\(fn_,v_) . fn_) fn_v_list)) ) ( ((MAP (\(fn_'',v_'') . fn_'') fn''_v''_list)) )) )) ==> ( ( JRbprim (Expr_record ((MAP (\(fn_,v_) . ((F_name fn_),v_)) fn_v_list))) Bprim_equal v' Lab_nil (FOLDR Expr_and (Expr_constant CONST_true) ((MAP (\(fn_,v_) . (Expr_apply (Expr_apply (Expr_bprim Bprim_equal) v_) (Expr_field v' (F_name fn_)) )) fn_v_list)) ) ))) /\ ( (* Jbprim_plus *) !(intn1:intn) (intn2:intn) . (clause_name "Jbprim_plus") ==> ( ( JRbprim (Expr_constant (CONST_int intn1)) Bprim_plus (Expr_constant (CONST_int intn2)) Lab_nil (Expr_constant (CONST_int ( intn1 + intn2 ) )) ))) /\ ( (* Jbprim_minus *) !(intn1:intn) (intn2:intn) . (clause_name "Jbprim_minus") ==> ( ( JRbprim (Expr_constant (CONST_int intn1)) Bprim_minus (Expr_constant (CONST_int intn2)) Lab_nil (Expr_constant (CONST_int ( intn1 - intn2 ) )) ))) /\ ( (* Jbprim_times *) !(intn1:intn) (intn2:intn) . (clause_name "Jbprim_times") ==> ( ( JRbprim (Expr_constant (CONST_int intn1)) Bprim_times (Expr_constant (CONST_int intn2)) Lab_nil (Expr_constant (CONST_int ( intn1 * intn2 ) )) ))) /\ ( (* Jbprim_div0 *) !(intn:intn) . (clause_name "Jbprim_div0") ==> ( ( JRbprim (Expr_constant (CONST_int intn)) Bprim_div (Expr_constant (CONST_int 0w )) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) (Expr_constant (CONST_constr C_div_by_0))) ))) /\ ( (* Jbprim_div *) !(intn1:intn) (intn2:intn) . (clause_name "Jbprim_div") /\ (( (~( (CONST_int intn2) = (CONST_int 0w ) )) )) ==> ( ( JRbprim (Expr_constant (CONST_int intn1)) Bprim_div (Expr_constant (CONST_int intn2)) Lab_nil (Expr_constant (CONST_int ( intn1 / intn2 ) )) ))) /\ ( (* Jbprim_assign *) !(l:index) (v:expr) . (clause_name "Jbprim_assign") /\ ((is_value_of_expr v)) ==> ( ( JRbprim (Expr_location l) Bprim_assign v (Lab_assign l v) (Expr_constant CONST_unit) ))) `; (* defns JRmatching_step *) val (JRmatching_step_rules, JRmatching_step_ind, JRmatching_step_cases) = Hol_reln ` (* defn matching_step *) ( (* JRmatching_next *) !(pat_e_list:(pattern#expr) list) (pat:pattern) (e:expr) (v:expr) . (clause_name "JRmatching_next") /\ ((is_value_of_expr v) /\ ( (~JM_matchP v pat ) ) /\ ( (LENGTH ( ((MAP (\(pat_,e_) . e_) pat_e_list)) ) >= 1 ) )) ==> ( ( JRmatching_step v (PM_pm ([((PE_inj pat e))] ++ (MAP (\(pat_,e_) . (PE_inj pat_ e_)) pat_e_list))) (PM_pm ((MAP (\(pat_,e_) . (PE_inj pat_ e_)) pat_e_list))) ))) `; (* defns JRmatching_success *) val (JRmatching_success_rules, JRmatching_success_ind, JRmatching_success_cases) = Hol_reln ` (* defn matching_success *) ( (* JRmatching_found *) !(x_v_list:(value_name#expr) list) (pat_e_list:(pattern#expr) list) (v:expr) (pat:pattern) (e:expr) . (clause_name "JRmatching_found") /\ ((is_value_of_expr v) /\ (EVERY (\(x_,v_). is_value_of_expr v_) x_v_list) /\ ( ( JM_match v pat (substs_x_xs (x_v_list)) ))) ==> ( ( JRmatching_success v (PM_pm ([((PE_inj pat e))] ++ (MAP (\(pat_,e_) . (PE_inj pat_ e_)) pat_e_list))) (substs_value_name_expr (case (substs_x_xs (x_v_list)) of substs_x_xs l -> l) e ) ))) /\ ( (* JRmatching_fail *) !(pat:pattern) (e:expr) (v:expr) . (clause_name "JRmatching_fail") /\ ((is_value_of_expr v) /\ ( (~JM_matchP v pat ) )) ==> ( ( JRmatching_success v (PM_pm ([((PE_inj pat e))])) (Expr_apply (Expr_uprim Uprim_raise) (Expr_constant (CONST_constr C_matchfailure))) ))) `; (* defns Jred *) val (Jred_rules, Jred_ind, Jred_cases) = Hol_reln ` (* defn expr *) ( (* JR_expr_uprim *) !(unary_prim:unary_prim) (v:expr) (L:trans_label) (e:expr) . (clause_name "JR_expr_uprim") /\ ((is_value_of_expr v) /\ ( ( JRuprim unary_prim v L e ))) ==> ( ( JR_expr (Expr_apply (Expr_uprim unary_prim) v) L e ))) /\ ( (* JR_expr_bprim *) !(binary_prim:binary_prim) (v1:expr) (v2:expr) (L:trans_label) (e:expr) . (clause_name "JR_expr_bprim") /\ ((is_value_of_expr v1) /\ (is_value_of_expr v2) /\ ( ( JRbprim v1 binary_prim v2 L e ))) ==> ( ( JR_expr (Expr_apply (Expr_apply (Expr_bprim binary_prim) v1) v2) L e ))) /\ ( (* JR_expr_typed_ctx *) !(e:expr) (t:typexpr) . (clause_name "JR_expr_typed_ctx") ==> ( ( JR_expr (Expr_typed e t) Lab_nil e ))) /\ ( (* JR_expr_apply_ctx_arg *) !(e1:expr) (e0:expr) (L:trans_label) (e0':expr) . (clause_name "JR_expr_apply_ctx_arg") /\ (( ( JR_expr e0 L e0' ))) ==> ( ( JR_expr (Expr_apply e1 e0) L (Expr_apply e1 e0') ))) /\ ( (* JR_expr_apply_raise1 *) !(e:expr) (v:expr) . (clause_name "JR_expr_apply_raise1") /\ ((is_value_of_expr v)) ==> ( ( JR_expr (Expr_apply e (Expr_apply (Expr_uprim Uprim_raise) v) ) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) ))) /\ ( (* JR_expr_apply_ctx_fun *) !(e1:expr) (v0:expr) (L:trans_label) (e1':expr) . (clause_name "JR_expr_apply_ctx_fun") /\ ((is_value_of_expr v0) /\ ( ( JR_expr e1 L e1' ))) ==> ( ( JR_expr (Expr_apply e1 v0) L (Expr_apply e1' v0) ))) /\ ( (* JR_expr_apply_raise2 *) !(v:expr) (v':expr) . (clause_name "JR_expr_apply_raise2") /\ ((is_value_of_expr v) /\ (is_value_of_expr v')) ==> ( ( JR_expr (Expr_apply (Expr_apply (Expr_uprim Uprim_raise) v) v') Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) ))) /\ ( (* JR_expr_apply *) !(pattern_matching:pattern_matching) (v0:expr) . (clause_name "JR_expr_apply") /\ ((is_value_of_expr v0)) ==> ( ( JR_expr (Expr_apply (Expr_function pattern_matching) v0) Lab_nil (Expr_match v0 pattern_matching) ))) /\ ( (* JR_expr_let_ctx *) !(pat:pattern) (e0:expr) (e:expr) (L:trans_label) (e0':expr) . (clause_name "JR_expr_let_ctx") /\ (( ( JR_expr e0 L e0' ))) ==> ( ( JR_expr (Expr_let (LB_simple pat e0) e) L (Expr_let (LB_simple pat e0') e) ))) /\ ( (* JR_expr_let_raise *) !(pat:pattern) (v:expr) (e:expr) . (clause_name "JR_expr_let_raise") /\ ((is_value_of_expr v)) ==> ( ( JR_expr (Expr_let (LB_simple pat (Expr_apply (Expr_uprim Uprim_raise) v)) e) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) ))) /\ ( (* JR_expr_let_subst *) !(x_v_list:(value_name#expr) list) (pat:pattern) (v:expr) (e:expr) . (clause_name "JR_expr_let_subst") /\ ((is_value_of_expr v) /\ (EVERY (\(x_,v_). is_value_of_expr v_) x_v_list) /\ ( ( JM_match v pat (substs_x_xs (x_v_list)) ))) ==> ( ( JR_expr (Expr_let (LB_simple pat v) e) Lab_nil (substs_value_name_expr (case (substs_x_xs (x_v_list)) of substs_x_xs l -> l) e ) ))) /\ ( (* JR_expr_let_fail *) !(pat:pattern) (e:expr) (v:expr) . (clause_name "JR_expr_let_fail") /\ ((is_value_of_expr v) /\ ( (~JM_matchP v pat ) )) ==> ( ( JR_expr (Expr_let (LB_simple pat v) e) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) (Expr_constant (CONST_constr C_matchfailure))) ))) /\ ( (* JR_expr_letrec *) !(x_e_pattern_matching_list:(value_name#expr#pattern_matching) list) (letrec_bindings:letrec_bindings) (e:expr) . (clause_name "JR_expr_letrec") /\ (( ( letrec_bindings = (LRBs_inj ((MAP (\(x_,e_,pattern_matching_) . (LRB_simple x_ pattern_matching_)) x_e_pattern_matching_list))) ) ) /\ ((EVERY (\ b . b) ((MAP (\(x_,e_,pattern_matching_) . ( Jrecfun letrec_bindings pattern_matching_ e_ )) x_e_pattern_matching_list))))) ==> ( ( JR_expr (Expr_letrec letrec_bindings e) Lab_nil (substs_value_name_expr (case (substs_x_xs ((MAP (\(x_,e_,pattern_matching_) . (x_,e_)) x_e_pattern_matching_list))) of substs_x_xs l -> l) e ) ))) /\ ( (* JR_expr_sequence_ctx_left *) !(e1:expr) (e2:expr) (L:trans_label) (e1':expr) . (clause_name "JR_expr_sequence_ctx_left") /\ (( ( JR_expr e1 L e1' ))) ==> ( ( JR_expr (Expr_sequence e1 e2) L (Expr_sequence e1' e2) ))) /\ ( (* JR_expr_sequence_raise *) !(v:expr) (e:expr) . (clause_name "JR_expr_sequence_raise") /\ ((is_value_of_expr v)) ==> ( ( JR_expr (Expr_sequence (Expr_apply (Expr_uprim Uprim_raise) v) e) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) ))) /\ ( (* JR_expr_sequence *) !(v:expr) (e2:expr) . (clause_name "JR_expr_sequence") /\ ((is_value_of_expr v)) ==> ( ( JR_expr (Expr_sequence v e2) Lab_nil e2 ))) /\ ( (* JR_expr_ifthenelse_ctx *) !(e1:expr) (e2:expr) (e3:expr) (L:trans_label) (e1':expr) . (clause_name "JR_expr_ifthenelse_ctx") /\ (( ( JR_expr e1 L e1' ))) ==> ( ( JR_expr (Expr_ifthenelse e1 e2 e3) L (Expr_ifthenelse e1' e2 e3) ))) /\ ( (* JR_expr_if_raise *) !(v:expr) (e1:expr) (e2:expr) . (clause_name "JR_expr_if_raise") /\ ((is_value_of_expr v)) ==> ( ( JR_expr (Expr_ifthenelse (Expr_apply (Expr_uprim Uprim_raise) v) e1 e2) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) ))) /\ ( (* JR_expr_ifthenelse_true *) !(e2:expr) (e3:expr) . (clause_name "JR_expr_ifthenelse_true") ==> ( ( JR_expr (Expr_ifthenelse (Expr_constant CONST_true) e2 e3) Lab_nil e2 ))) /\ ( (* JR_expr_ifthenelse_false *) !(e2:expr) (e3:expr) . (clause_name "JR_expr_ifthenelse_false") ==> ( ( JR_expr (Expr_ifthenelse (Expr_constant CONST_false) e2 e3) Lab_nil e3 ))) /\ ( (* JR_expr_match_ctx *) !(e:expr) (pattern_matching:pattern_matching) (L:trans_label) (e':expr) . (clause_name "JR_expr_match_ctx") /\ (( ( JR_expr e L e' ))) ==> ( ( JR_expr (Expr_match e pattern_matching) L (Expr_match e' pattern_matching) ))) /\ ( (* JR_expr_match_raise *) !(v:expr) (pattern_matching:pattern_matching) . (clause_name "JR_expr_match_raise") /\ ((is_value_of_expr v)) ==> ( ( JR_expr (Expr_match (Expr_apply (Expr_uprim Uprim_raise) v) pattern_matching) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) ))) /\ ( (* JR_expr_match_step *) !(v:expr) (pattern_matching:pattern_matching) (pattern_matching':pattern_matching) . (clause_name "JR_expr_match_step") /\ ((is_value_of_expr v) /\ ( ( JRmatching_step v pattern_matching pattern_matching' ))) ==> ( ( JR_expr (Expr_match v pattern_matching) Lab_nil (Expr_match v pattern_matching') ))) /\ ( (* JR_expr_match_success *) !(v:expr) (pattern_matching:pattern_matching) (e':expr) . (clause_name "JR_expr_match_success") /\ ((is_value_of_expr v) /\ ( ( JRmatching_success v pattern_matching e' ))) ==> ( ( JR_expr (Expr_match v pattern_matching) Lab_nil e' ))) /\ ( (* JR_expr_and *) !(e1:expr) (e2:expr) . (clause_name "JR_expr_and") ==> ( ( JR_expr (Expr_and e1 e2) Lab_nil (Expr_ifthenelse e1 e2 (Expr_constant CONST_false)) ))) /\ ( (* JR_expr_or *) !(e1:expr) (e2:expr) . (clause_name "JR_expr_or") ==> ( ( JR_expr (Expr_or e1 e2) Lab_nil (Expr_ifthenelse e1 (Expr_constant CONST_true) e2) ))) /\ ( (* JR_expr_while *) !(e1:expr) (e2:expr) . (clause_name "JR_expr_while") ==> ( ( JR_expr (Expr_while e1 e2) Lab_nil (Expr_ifthenelse e1 (Expr_sequence e2 (Expr_while e1 e2)) (Expr_constant CONST_unit)) ))) /\ ( (* JR_expr_for_ctx1 *) !(x:value_name) (e1:expr) (for_dirn:for_dirn) (e2:expr) (e3:expr) (L:trans_label) (e1':expr) . (clause_name "JR_expr_for_ctx1") /\ (( ( JR_expr e1 L e1' ))) ==> ( ( JR_expr (Expr_for x e1 for_dirn e2 e3) L (Expr_for x e1' for_dirn e2 e3) ))) /\ ( (* JR_expr_for_raise1 *) !(x:value_name) (v:expr) (for_dirn:for_dirn) (e2:expr) (e3:expr) . (clause_name "JR_expr_for_raise1") /\ ((is_value_of_expr v)) ==> ( ( JR_expr (Expr_for x (Expr_apply (Expr_uprim Uprim_raise) v) for_dirn e2 e3) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) ))) /\ ( (* JR_expr_for_ctx2 *) !(x:value_name) (v1:expr) (for_dirn:for_dirn) (e2:expr) (e3:expr) (L:trans_label) (e2':expr) . (clause_name "JR_expr_for_ctx2") /\ ((is_value_of_expr v1) /\ ( ( JR_expr e2 L e2' ))) ==> ( ( JR_expr (Expr_for x v1 for_dirn e2 e3) L (Expr_for x v1 for_dirn e2' e3) ))) /\ ( (* JR_expr_for_raise2 *) !(x:value_name) (v:expr) (for_dirn:for_dirn) (v':expr) (e3:expr) . (clause_name "JR_expr_for_raise2") /\ ((is_value_of_expr v) /\ (is_value_of_expr v')) ==> ( ( JR_expr (Expr_for x v for_dirn (Expr_apply (Expr_uprim Uprim_raise) v') e3) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v') ))) /\ ( (* JR_expr_for_to_do *) !(x:value_name) (intn1:intn) (intn2:intn) (e:expr) . (clause_name "JR_expr_for_to_do") /\ (( ( intn1 <= intn2 ) )) ==> ( ( JR_expr (Expr_for x (Expr_constant (CONST_int intn1)) FD_upto (Expr_constant (CONST_int intn2)) e) Lab_nil (Expr_sequence (Expr_let (LB_simple (P_var x) (Expr_constant (CONST_int intn1))) e) (Expr_for x (Expr_constant (CONST_int ( intn1 + 1w ) )) FD_upto (Expr_constant (CONST_int intn2)) e)) ))) /\ ( (* JR_expr_for_to_done *) !(x:value_name) (intn1:intn) (intn2:intn) (e:expr) . (clause_name "JR_expr_for_to_done") /\ (( ( intn1 > intn2 ) )) ==> ( ( JR_expr (Expr_for x (Expr_constant (CONST_int intn1)) FD_upto (Expr_constant (CONST_int intn2)) e) Lab_nil (Expr_constant CONST_unit) ))) /\ ( (* JR_expr_for_downto_do *) !(x:value_name) (intn1:intn) (intn2:intn) (e:expr) . (clause_name "JR_expr_for_downto_do") /\ (( ( intn2 <= intn1 ) )) ==> ( ( JR_expr (Expr_for x (Expr_constant (CONST_int intn1)) FD_downto (Expr_constant (CONST_int intn2)) e) Lab_nil (Expr_sequence (Expr_let (LB_simple (P_var x) (Expr_constant (CONST_int intn1))) e) (Expr_for x (Expr_constant (CONST_int ( intn1 - 1w ) )) FD_downto (Expr_constant (CONST_int intn2)) e)) ))) /\ ( (* JR_expr_for_downto_done *) !(x:value_name) (intn1:intn) (intn2:intn) (e:expr) . (clause_name "JR_expr_for_downto_done") /\ (( ( intn2 > intn1 ) )) ==> ( ( JR_expr (Expr_for x (Expr_constant (CONST_int intn1)) FD_downto (Expr_constant (CONST_int intn2)) e) Lab_nil (Expr_constant CONST_unit) ))) /\ ( (* JR_expr_try_ctx *) !(e:expr) (pattern_matching:pattern_matching) (L:trans_label) (e':expr) . (clause_name "JR_expr_try_ctx") /\ (( ( JR_expr e L e' ))) ==> ( ( JR_expr (Expr_try e pattern_matching) L (Expr_try e' pattern_matching) ))) /\ ( (* JR_expr_try_return *) !(v:expr) (pattern_matching:pattern_matching) . (clause_name "JR_expr_try_return") /\ ((is_value_of_expr v)) ==> ( ( JR_expr (Expr_try v pattern_matching) Lab_nil v ))) /\ ( (* JR_expr_try_catch *) !(pat_exp_list:pat_exp list) (v:expr) . (clause_name "JR_expr_try_catch") /\ ((is_value_of_expr v)) ==> ( ( JR_expr (Expr_try (Expr_apply (Expr_uprim Uprim_raise) v) (PM_pm (pat_exp_list))) Lab_nil (Expr_match v (PM_pm (pat_exp_list ++ [((PE_inj P_any (Expr_apply (Expr_uprim Uprim_raise) v) ))]))) ))) /\ ( (* JR_expr_tuple_ctx *) !(v_list:expr list) (e_list:expr list) (e:expr) (L:trans_label) (e':expr) . (clause_name "JR_expr_tuple_ctx") /\ ((EVERY (\v_. is_value_of_expr v_) v_list) /\ ( ( JR_expr e L e' ))) ==> ( ( JR_expr (Expr_tuple (e_list ++ [(e)] ++ v_list)) L (Expr_tuple (e_list ++ [(e')] ++ v_list)) ))) /\ ( (* JR_expr_tuple_raise *) !(v_list:expr list) (e_list:expr list) (v:expr) . (clause_name "JR_expr_tuple_raise") /\ ((is_value_of_expr v) /\ (EVERY (\v_. is_value_of_expr v_) v_list)) ==> ( ( JR_expr (Expr_tuple (e_list ++ [( (Expr_apply (Expr_uprim Uprim_raise) v) )] ++ v_list)) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) ))) /\ ( (* JR_expr_constr_ctx *) !(v_list:expr list) (e_list:expr list) (constr:constr) (e:expr) (L:trans_label) (e':expr) . (clause_name "JR_expr_constr_ctx") /\ ((EVERY (\v_. is_value_of_expr v_) v_list) /\ ( ( JR_expr e L e' ))) ==> ( ( JR_expr (Expr_construct constr (e_list ++ [(e)] ++ v_list)) L (Expr_construct constr (e_list ++ [(e')] ++ v_list)) ))) /\ ( (* JR_expr_constr_raise *) !(v_list:expr list) (e_list:expr list) (constr:constr) (v:expr) . (clause_name "JR_expr_constr_raise") /\ ((is_value_of_expr v) /\ (EVERY (\v_. is_value_of_expr v_) v_list)) ==> ( ( JR_expr (Expr_construct constr (e_list ++ [( (Expr_apply (Expr_uprim Uprim_raise) v) )] ++ v_list)) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) ))) /\ ( (* JR_expr_cons_ctx1 *) !(e0:expr) (e:expr) (L:trans_label) (e':expr) . (clause_name "JR_expr_cons_ctx1") /\ (( ( JR_expr e L e' ))) ==> ( ( JR_expr (Expr_cons e0 e) L (Expr_cons e0 e') ))) /\ ( (* JR_expr_cons_raise1 *) !(e:expr) (v:expr) . (clause_name "JR_expr_cons_raise1") /\ ((is_value_of_expr v)) ==> ( ( JR_expr (Expr_cons e (Expr_apply (Expr_uprim Uprim_raise) v) ) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) ))) /\ ( (* JR_expr_cons_ctx2 *) !(e:expr) (v:expr) (L:trans_label) (e':expr) . (clause_name "JR_expr_cons_ctx2") /\ ((is_value_of_expr v) /\ ( ( JR_expr e L e' ))) ==> ( ( JR_expr (Expr_cons e v) L (Expr_cons e' v) ))) /\ ( (* JR_expr_cons_raise2 *) !(v:expr) (v':expr) . (clause_name "JR_expr_cons_raise2") /\ ((is_value_of_expr v) /\ (is_value_of_expr v')) ==> ( ( JR_expr (Expr_cons (Expr_apply (Expr_uprim Uprim_raise) v) v') Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) ))) /\ ( (* JR_expr_record_ctx *) !(fn'_v_list:(field_name#expr) list) (fn_e_list:(field_name#expr) list) (field_name:field_name) (expr:expr) (L:trans_label) (expr':expr) . (clause_name "JR_expr_record_ctx") /\ ((EVERY (\(fn_',v_). is_value_of_expr v_) fn'_v_list) /\ ( ( JR_expr expr L expr' ))) ==> ( ( JR_expr (Expr_record ((MAP (\(fn_,e_) . ((F_name fn_),e_)) fn_e_list) ++ [((F_name field_name),expr)] ++ (MAP (\(fn_',v_) . ((F_name fn_'),v_)) fn'_v_list))) L (Expr_record ((MAP (\(fn_,e_) . ((F_name fn_),e_)) fn_e_list) ++ [((F_name field_name),expr')] ++ (MAP (\(fn_',v_) . ((F_name fn_'),v_)) fn'_v_list))) ))) /\ ( (* JR_expr_record_raise *) !(fn'_v_list:(field_name#expr) list) (fn_e_list:(field_name#expr) list) (fn:field_name) (v:expr) . (clause_name "JR_expr_record_raise") /\ ((is_value_of_expr v) /\ (EVERY (\(fn_',v_). is_value_of_expr v_) fn'_v_list)) ==> ( ( JR_expr (Expr_record ((MAP (\(fn_,e_) . ((F_name fn_),e_)) fn_e_list) ++ [((F_name fn),(Expr_apply (Expr_uprim Uprim_raise) v))] ++ (MAP (\(fn_',v_) . ((F_name fn_'),v_)) fn'_v_list))) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) ))) /\ ( (* JR_expr_record_with_ctx1 *) !(fn'_v_list:(field_name#expr) list) (fn_e_list:(field_name#expr) list) (v:expr) (field_name:field_name) (e:expr) (L:trans_label) (e':expr) . (clause_name "JR_expr_record_with_ctx1") /\ ((is_value_of_expr v) /\ (EVERY (\(fn_',v_). is_value_of_expr v_) fn'_v_list) /\ ( ( JR_expr e L e' ))) ==> ( ( JR_expr (Expr_override v ((MAP (\(fn_,e_) . ((F_name fn_),e_)) fn_e_list) ++ [((F_name field_name),e)] ++ (MAP (\(fn_',v_) . ((F_name fn_'),v_)) fn'_v_list))) L (Expr_override v ((MAP (\(fn_,e_) . ((F_name fn_),e_)) fn_e_list) ++ [((F_name field_name),e')] ++ (MAP (\(fn_',v_) . ((F_name fn_'),v_)) fn'_v_list))) ))) /\ ( (* JR_expr_record_with_raise1 *) !(fn'_v_list:(field_name#expr) list) (fn_e_list:(field_name#expr) list) (v':expr) (fn:field_name) (v:expr) . (clause_name "JR_expr_record_with_raise1") /\ ((is_value_of_expr v') /\ (is_value_of_expr v) /\ (EVERY (\(fn_',v_). is_value_of_expr v_) fn'_v_list)) ==> ( ( JR_expr (Expr_override v' ((MAP (\(fn_,e_) . ((F_name fn_),e_)) fn_e_list) ++ [((F_name fn),(Expr_apply (Expr_uprim Uprim_raise) v))] ++ (MAP (\(fn_',v_) . ((F_name fn_'),v_)) fn'_v_list))) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) ))) /\ ( (* JR_expr_record_with_ctx2 *) !(field_name_e_list:(field_name#expr) list) (e:expr) (L:trans_label) (e':expr) . (clause_name "JR_expr_record_with_ctx2") /\ (( ( JR_expr e L e' ))) ==> ( ( JR_expr (Expr_override e ((MAP (\(field_name_,e_) . ((F_name field_name_),e_)) field_name_e_list))) L (Expr_override e' ((MAP (\(field_name_,e_) . ((F_name field_name_),e_)) field_name_e_list))) ))) /\ ( (* JR_expr_record_raise_ctx2 *) !(field_name_e_list:(field_name#expr) list) (v:expr) . (clause_name "JR_expr_record_raise_ctx2") /\ ((is_value_of_expr v)) ==> ( ( JR_expr (Expr_override (Expr_apply (Expr_uprim Uprim_raise) v) ((MAP (\(field_name_,e_) . ((F_name field_name_),e_)) field_name_e_list))) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) ))) /\ ( (* JR_expr_record_with_many *) !(fn''_v''_list:(field_name#expr) list) (fn'_v'_list:(field_name#expr) list) (fn_v_list:(field_name#expr) list) (field_name:field_name) (v:expr) (v':expr) . (clause_name "JR_expr_record_with_many") /\ ((is_value_of_expr v) /\ (is_value_of_expr v') /\ (EVERY (\(fn_'',v_''). is_value_of_expr v_'') fn''_v''_list) /\ (EVERY (\(fn_',v_'). is_value_of_expr v_') fn'_v'_list) /\ (EVERY (\(fn_,v_). is_value_of_expr v_) fn_v_list) /\ ( (LENGTH ( ((MAP (\(fn_'',v_'') . v_'') fn''_v''_list)) ) >= 1 ) ) /\ ( (~MEM (name_fn field_name) ((MAP (\(fn_,v_) . (name_fn fn_)) fn_v_list)) ) )) ==> ( ( JR_expr (Expr_override (Expr_record ((MAP (\(fn_,v_) . ((F_name fn_),v_)) fn_v_list) ++ [((F_name field_name),v)] ++ (MAP (\(fn_',v_') . ((F_name fn_'),v_')) fn'_v'_list))) ([((F_name field_name),v')] ++ (MAP (\(fn_'',v_'') . ((F_name fn_''),v_'')) fn''_v''_list))) Lab_nil (Expr_override (Expr_record ((MAP (\(fn_,v_) . ((F_name fn_),v_)) fn_v_list) ++ [((F_name field_name),v')] ++ (MAP (\(fn_',v_') . ((F_name fn_'),v_')) fn'_v'_list))) ((MAP (\(fn_'',v_'') . ((F_name fn_''),v_'')) fn''_v''_list))) ))) /\ ( (* JR_expr_record_with_1 *) !(fn'_v'_list:(field_name#expr) list) (fn_v_list:(field_name#expr) list) (field_name:field_name) (v:expr) (v':expr) . (clause_name "JR_expr_record_with_1") /\ ((is_value_of_expr v) /\ (is_value_of_expr v') /\ (EVERY (\(fn_',v_'). is_value_of_expr v_') fn'_v'_list) /\ (EVERY (\(fn_,v_). is_value_of_expr v_) fn_v_list) /\ ( (~MEM (name_fn field_name) ((MAP (\(fn_,v_) . (name_fn fn_)) fn_v_list)) ) )) ==> ( ( JR_expr (Expr_override (Expr_record ((MAP (\(fn_,v_) . ((F_name fn_),v_)) fn_v_list) ++ [((F_name field_name),v)] ++ (MAP (\(fn_',v_') . ((F_name fn_'),v_')) fn'_v'_list))) ([((F_name field_name),v')])) Lab_nil (Expr_record ((MAP (\(fn_,v_) . ((F_name fn_),v_)) fn_v_list) ++ [((F_name field_name),v')] ++ (MAP (\(fn_',v_') . ((F_name fn_'),v_')) fn'_v'_list))) ))) /\ ( (* JR_expr_record_access_ctx *) !(e:expr) (field_name:field_name) (L:trans_label) (e':expr) . (clause_name "JR_expr_record_access_ctx") /\ (( ( JR_expr e L e' ))) ==> ( ( JR_expr (Expr_field e (F_name field_name)) L (Expr_field e' (F_name field_name)) ))) /\ ( (* JR_expr_record_access_raise *) !(v:expr) (field_name:field_name) . (clause_name "JR_expr_record_access_raise") /\ ((is_value_of_expr v)) ==> ( ( JR_expr (Expr_field (Expr_apply (Expr_uprim Uprim_raise) v) (F_name field_name)) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) ))) /\ ( (* JR_expr_record_access *) !(fn'_v'_list:(field_name#expr) list) (fn_v_list:(field_name#expr) list) (field_name:field_name) (v:expr) . (clause_name "JR_expr_record_access") /\ ((is_value_of_expr v) /\ (EVERY (\(fn_',v_'). is_value_of_expr v_') fn'_v'_list) /\ (EVERY (\(fn_,v_). is_value_of_expr v_) fn_v_list) /\ ( (~MEM (name_fn field_name) ((MAP (\(fn_,v_) . (name_fn fn_)) fn_v_list)) ) )) ==> ( ( JR_expr (Expr_field (Expr_record ((MAP (\(fn_,v_) . ((F_name fn_),v_)) fn_v_list) ++ [((F_name field_name),v)] ++ (MAP (\(fn_',v_') . ((F_name fn_'),v_')) fn'_v'_list))) (F_name field_name)) Lab_nil v ))) /\ ( (* JR_expr_assert_ctx *) !(e:expr) (L:trans_label) (e':expr) . (clause_name "JR_expr_assert_ctx") /\ (( ( JR_expr e L e' ))) ==> ( ( JR_expr (Expr_assert e) L (Expr_assert e') ))) /\ ( (* JR_expr_assert_raise *) !(v:expr) . (clause_name "JR_expr_assert_raise") /\ ((is_value_of_expr v)) ==> ( ( JR_expr (Expr_assert (Expr_apply (Expr_uprim Uprim_raise) v) ) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) ))) /\ ( (* JR_expr_assert_true *) (clause_name "JR_expr_assert_true") ==> ( ( JR_expr (Expr_assert (Expr_constant CONST_true)) Lab_nil (Expr_constant CONST_unit) ))) /\ ( (* JR_expr_assert_false *) (clause_name "JR_expr_assert_false") ==> ( ( JR_expr (Expr_assert (Expr_constant CONST_false)) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) (Expr_constant (CONST_constr C_assertfailure))) ))) `; (* defns JRdefn *) val (JRdefn_rules, JRdefn_ind, JRdefn_cases) = Hol_reln ` (* defn Rdefn *) ( (* Jdefn_let_ctx *) !(ds_value:definitions) (pat:pattern) (e:expr) (definitions:definitions) (L:trans_label) (e':expr) . (clause_name "Jdefn_let_ctx") /\ ((is_definitions_value_of_definitions ds_value) /\ ( ( JR_expr e L e' ))) ==> ( ( JRdefn ds_value (Prog_defs (Ds_cons (D_let (LB_simple pat e)) definitions ) ) L ds_value (Prog_defs (Ds_cons (D_let (LB_simple pat e')) definitions ) ) ))) /\ ( (* Jdefn_let_raise *) !(ds_value:definitions) (pat:pattern) (v:expr) (definitions:definitions) . (clause_name "Jdefn_let_raise") /\ ((is_definitions_value_of_definitions ds_value) /\ (is_value_of_expr v)) ==> ( ( JRdefn ds_value (Prog_defs (Ds_cons (D_let (LB_simple pat (Expr_apply (Expr_uprim Uprim_raise) v))) definitions ) ) Lab_nil ds_value (Prog_raise v) ))) /\ ( (* Jdefn_let_match *) !(x_v_list:(value_name#expr) list) (ds_value:definitions) (pat:pattern) (v:expr) (definitions:definitions) . (clause_name "Jdefn_let_match") /\ ((is_definitions_value_of_definitions ds_value) /\ (is_value_of_expr v) /\ (EVERY (\(x_,v_). is_value_of_expr v_) x_v_list) /\ ( ( JM_match v pat (substs_x_xs (x_v_list)) ))) ==> ( ( JRdefn ds_value (Prog_defs (Ds_cons (D_let (LB_simple pat v)) definitions ) ) Lab_nil ds_value (Prog_defs (substs_value_name_definitions (case (substs_x_xs ((MAP (\(x_,v_) . (x_, (remv_tyvar_expr v_ ) )) x_v_list))) of substs_x_xs l -> l) definitions ) ) ))) /\ ( (* Jdefn_let_not_match *) !(ds_value:definitions) (pat:pattern) (definitions:definitions) (v:expr) . (clause_name "Jdefn_let_not_match") /\ ((is_definitions_value_of_definitions ds_value) /\ (is_value_of_expr v) /\ ( (~JM_matchP v pat ) )) ==> ( ( JRdefn ds_value (Prog_defs (Ds_cons (D_let (LB_simple pat v)) definitions ) ) Lab_nil ds_value (Prog_raise (Expr_constant (CONST_constr C_matchfailure))) ))) /\ ( (* Jdefn_letrec *) !(x_e_pattern_matching_list:(value_name#expr#pattern_matching) list) (ds_value:definitions) (letrec_bindings:letrec_bindings) (definitions:definitions) . (clause_name "Jdefn_letrec") /\ ((is_definitions_value_of_definitions ds_value) /\ ( ( letrec_bindings = (LRBs_inj ((MAP (\(x_,e_,pattern_matching_) . (LRB_simple x_ pattern_matching_)) x_e_pattern_matching_list))) ) ) /\ ((EVERY (\ b . b) ((MAP (\(x_,e_,pattern_matching_) . ( Jrecfun letrec_bindings pattern_matching_ e_ )) x_e_pattern_matching_list))))) ==> ( ( JRdefn ds_value (Prog_defs (Ds_cons (D_letrec letrec_bindings) definitions ) ) Lab_nil ds_value (Prog_defs (substs_value_name_definitions (case (substs_x_xs ((MAP (\(x_,e_,pattern_matching_) . (x_, (remv_tyvar_expr e_ ) )) x_e_pattern_matching_list))) of substs_x_xs l -> l) definitions ) ) ))) /\ ( (* Jdefn_type *) !(ds_value:definitions) (type_definition:type_definition) (definitions:definitions) . (clause_name "Jdefn_type") /\ ((is_definitions_value_of_definitions ds_value)) ==> ( ( JRdefn ds_value (Prog_defs (Ds_cons (D_type type_definition) definitions ) ) Lab_nil (definitions_snoc ds_value (D_type type_definition) ) (Prog_defs definitions) ))) /\ ( (* Jdefn_exn *) !(ds_value:definitions) (exception_definition:exception_definition) (definitions:definitions) . (clause_name "Jdefn_exn") /\ ((is_definitions_value_of_definitions ds_value)) ==> ( ( JRdefn ds_value (Prog_defs (Ds_cons (D_exception exception_definition) definitions ) ) Lab_nil (definitions_snoc ds_value (D_exception exception_definition) ) (Prog_defs definitions) ))) `; (* defns JSlookup *) val (JSlookup_rules, JSlookup_ind, JSlookup_cases) = Hol_reln ` (* defn lookup *) ( (* JSstlookup_rec *) !(st:store) (l':index) (e:expr) (l:index) (e':expr) . (clause_name "JSstlookup_rec") /\ (( ( JSlookup st l e' )) /\ ( (~( (name_l l) = (name_l l') )) )) ==> ( ( JSlookup (( l' , e ):: st ) l e' ))) /\ ( (* JSstlookup_found *) !(st:store) (l:index) (e:expr) . (clause_name "JSstlookup_found") ==> ( ( JSlookup (( l , e ):: st ) l e ))) `; (* defns JRstore *) val (JRstore_rules, JRstore_ind, JRstore_cases) = Hol_reln ` (* defn store *) ( (* JRstore_empty *) !(st:store) . (clause_name "JRstore_empty") ==> ( ( JRstore st Lab_nil st ))) /\ ( (* JRstore_lookup *) !(st:store) (l:index) (v:expr) . (clause_name "JRstore_lookup") /\ ((is_value_of_expr v) /\ ( ( JSlookup st l v ))) ==> ( ( JRstore st (Lab_deref l v) st ))) /\ ( (* JRstore_assign *) !(st:store) (l:index) (expr:expr) (st':store) (v:expr) . (clause_name "JRstore_assign") /\ ((is_value_of_expr v) /\ ( (!v8. ~JSlookup st' l v8) )) ==> ( ( JRstore ( st' ++[( l , expr )]++ st ) (Lab_assign l v) ( st' ++[( l , (remv_tyvar_expr v ) )]++ st ) ))) /\ ( (* JRstore_alloc *) !(st:store) (l:index) (v:expr) . (clause_name "JRstore_alloc") /\ ((is_value_of_expr v) /\ ( (!v8. ~JSlookup st l v8) )) ==> ( ( JRstore st (Lab_alloc v l) (( l , (remv_tyvar_expr v ) ):: st ) ))) `; (* defns JRtop *) val (JRtop_rules, JRtop_ind, JRtop_cases) = Hol_reln ` (* defn top *) ( (* JRtop_defs *) !(definitions_value:definitions) (program:program) (store:store) (definitions:definitions) (program':program) (store':store) (L:trans_label) . (clause_name "JRtop_defs") /\ ((is_definitions_value_of_definitions definitions_value) /\ ( ( JRstore store L store' )) /\ ( ( JRdefn definitions_value program L definitions program' ))) ==> ( ( JRtop definitions_value program store definitions program' store' ))) `; (* defns Jebehaviour *) val (Jebehaviour_rules, Jebehaviour_ind, Jebehaviour_cases) = Hol_reln ` (* defn ebehaviour *) ( (* JRB_ebehaviour_value *) !(v:expr) . (clause_name "JRB_ebehaviour_value") /\ ((is_value_of_expr v)) ==> ( ( JRB_ebehaviour v ))) /\ ( (* JRB_ebehaviour_reduces *) !(e:expr) (L:trans_label) (e':expr) . (clause_name "JRB_ebehaviour_reduces") /\ (( ( JR_expr e L e' ))) ==> ( ( JRB_ebehaviour e ))) /\ ( (* JRB_ebehaviour_raises *) !(v:expr) . (clause_name "JRB_ebehaviour_raises") /\ ((is_value_of_expr v)) ==> ( ( JRB_ebehaviour (Expr_apply (Expr_uprim Uprim_raise) v) ))) `; (* defns Jdbehaviour *) val (Jdbehaviour_rules, Jdbehaviour_ind, Jdbehaviour_cases) = Hol_reln ` (* defn dbehaviour *) ( (* JRB_behaviour_value *) !(definitions_value:definitions) (store:store) . (clause_name "JRB_behaviour_value") /\ ((is_definitions_value_of_definitions definitions_value)) ==> ( ( JRB_dbehaviour definitions_value (Prog_defs Ds_nil) store ))) /\ ( (* JRB_behaviour_reduces *) !(definitions_value:definitions) (program:program) (store:store) (definitions':definitions) (program':program) (store':store) . (clause_name "JRB_behaviour_reduces") /\ ((is_definitions_value_of_definitions definitions_value) /\ ( ( JRtop definitions_value program store definitions' program' store' ))) ==> ( ( JRB_dbehaviour definitions_value program store ))) /\ ( (* JRB_behaviour_raises *) !(definitions_value:definitions) (v:expr) (store:store) . (clause_name "JRB_behaviour_raises") /\ ((is_definitions_value_of_definitions definitions_value) /\ (is_value_of_expr v)) ==> ( ( JRB_dbehaviour definitions_value (Prog_raise v) store ))) `; val _ = export_theory ();