src/HOL/Import/HOL/prob_canon.imp
changeset 14516 a183dec876ab
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/HOL/prob_canon.imp	Fri Apr 02 17:37:45 2004 +0200
@@ -0,0 +1,147 @@
+import
+
+import_segment "hol4"
+
+def_maps
+  "algebra_canon" > "algebra_canon_primdef"
+  "alg_twinfree" > "alg_twinfree_primdef"
+  "alg_twin" > "alg_twin_primdef"
+  "alg_sorted" > "alg_sorted_primdef"
+  "alg_prefixfree" > "alg_prefixfree_primdef"
+  "alg_order_tupled" > "alg_order_tupled_def"
+  "alg_order" > "alg_order_primdef"
+  "alg_longest" > "alg_longest_primdef"
+  "alg_canon_prefs" > "alg_canon_prefs_primdef"
+  "alg_canon_merge" > "alg_canon_merge_primdef"
+  "alg_canon_find" > "alg_canon_find_primdef"
+  "alg_canon2" > "alg_canon2_primdef"
+  "alg_canon1" > "alg_canon1_primdef"
+  "alg_canon" > "alg_canon_primdef"
+
+const_maps
+  "algebra_canon" > "HOL4Prob.prob_canon.algebra_canon"
+  "alg_twinfree" > "HOL4Prob.prob_canon.alg_twinfree"
+  "alg_twin" > "HOL4Prob.prob_canon.alg_twin"
+  "alg_sorted" > "HOL4Prob.prob_canon.alg_sorted"
+  "alg_prefixfree" > "HOL4Prob.prob_canon.alg_prefixfree"
+  "alg_order_tupled" > "HOL4Prob.prob_canon.alg_order_tupled"
+  "alg_order" > "HOL4Prob.prob_canon.alg_order"
+  "alg_longest" > "HOL4Prob.prob_canon.alg_longest"
+  "alg_canon2" > "HOL4Prob.prob_canon.alg_canon2"
+  "alg_canon1" > "HOL4Prob.prob_canon.alg_canon1"
+  "alg_canon" > "HOL4Prob.prob_canon.alg_canon"
+
+thm_maps
+  "algebra_canon_primdef" > "HOL4Prob.prob_canon.algebra_canon_primdef"
+  "algebra_canon_def" > "HOL4Prob.prob_canon.algebra_canon_def"
+  "alg_twinfree_primitive_def" > "HOL4Prob.prob_canon.alg_twinfree_primitive_def"
+  "alg_twinfree_primdef" > "HOL4Prob.prob_canon.alg_twinfree_primdef"
+  "alg_twinfree_ind" > "HOL4Prob.prob_canon.alg_twinfree_ind"
+  "alg_twinfree_def" > "HOL4Prob.prob_canon.alg_twinfree_def"
+  "alg_twin_primdef" > "HOL4Prob.prob_canon.alg_twin_primdef"
+  "alg_twin_def" > "HOL4Prob.prob_canon.alg_twin_def"
+  "alg_sorted_primitive_def" > "HOL4Prob.prob_canon.alg_sorted_primitive_def"
+  "alg_sorted_primdef" > "HOL4Prob.prob_canon.alg_sorted_primdef"
+  "alg_sorted_ind" > "HOL4Prob.prob_canon.alg_sorted_ind"
+  "alg_sorted_def" > "HOL4Prob.prob_canon.alg_sorted_def"
+  "alg_prefixfree_primitive_def" > "HOL4Prob.prob_canon.alg_prefixfree_primitive_def"
+  "alg_prefixfree_primdef" > "HOL4Prob.prob_canon.alg_prefixfree_primdef"
+  "alg_prefixfree_ind" > "HOL4Prob.prob_canon.alg_prefixfree_ind"
+  "alg_prefixfree_def" > "HOL4Prob.prob_canon.alg_prefixfree_def"
+  "alg_order_tupled_primitive_def" > "HOL4Prob.prob_canon.alg_order_tupled_primitive_def"
+  "alg_order_tupled_def" > "HOL4Prob.prob_canon.alg_order_tupled_def"
+  "alg_order_primdef" > "HOL4Prob.prob_canon.alg_order_primdef"
+  "alg_order_ind" > "HOL4Prob.prob_canon.alg_order_ind"
+  "alg_order_def" > "HOL4Prob.prob_canon.alg_order_def"
+  "alg_order_curried_def" > "HOL4Prob.prob_canon.alg_order_curried_def"
+  "alg_longest_primdef" > "HOL4Prob.prob_canon.alg_longest_primdef"
+  "alg_longest_def" > "HOL4Prob.prob_canon.alg_longest_def"
+  "alg_canon_primdef" > "HOL4Prob.prob_canon.alg_canon_primdef"
+  "alg_canon_prefs_def" > "HOL4Prob.prob_canon.alg_canon_prefs_def"
+  "alg_canon_merge_def" > "HOL4Prob.prob_canon.alg_canon_merge_def"
+  "alg_canon_find_def" > "HOL4Prob.prob_canon.alg_canon_find_def"
+  "alg_canon_def" > "HOL4Prob.prob_canon.alg_canon_def"
+  "alg_canon2_primdef" > "HOL4Prob.prob_canon.alg_canon2_primdef"
+  "alg_canon2_def" > "HOL4Prob.prob_canon.alg_canon2_def"
+  "alg_canon1_primdef" > "HOL4Prob.prob_canon.alg_canon1_primdef"
+  "alg_canon1_def" > "HOL4Prob.prob_canon.alg_canon1_def"
+  "MEM_NIL_STEP" > "HOL4Prob.prob_canon.MEM_NIL_STEP"
+  "ALG_TWIN_SING" > "HOL4Prob.prob_canon.ALG_TWIN_SING"
+  "ALG_TWIN_REDUCE" > "HOL4Prob.prob_canon.ALG_TWIN_REDUCE"
+  "ALG_TWIN_NIL" > "HOL4Prob.prob_canon.ALG_TWIN_NIL"
+  "ALG_TWIN_CONS" > "HOL4Prob.prob_canon.ALG_TWIN_CONS"
+  "ALG_TWINS_PREFIX" > "HOL4Prob.prob_canon.ALG_TWINS_PREFIX"
+  "ALG_TWINFREE_TLS" > "HOL4Prob.prob_canon.ALG_TWINFREE_TLS"
+  "ALG_TWINFREE_TL" > "HOL4Prob.prob_canon.ALG_TWINFREE_TL"
+  "ALG_TWINFREE_STEP2" > "HOL4Prob.prob_canon.ALG_TWINFREE_STEP2"
+  "ALG_TWINFREE_STEP1" > "HOL4Prob.prob_canon.ALG_TWINFREE_STEP1"
+  "ALG_TWINFREE_STEP" > "HOL4Prob.prob_canon.ALG_TWINFREE_STEP"
+  "ALG_SORTED_TLS" > "HOL4Prob.prob_canon.ALG_SORTED_TLS"
+  "ALG_SORTED_TL" > "HOL4Prob.prob_canon.ALG_SORTED_TL"
+  "ALG_SORTED_STEP" > "HOL4Prob.prob_canon.ALG_SORTED_STEP"
+  "ALG_SORTED_PREFIXFREE_MEM_NIL" > "HOL4Prob.prob_canon.ALG_SORTED_PREFIXFREE_MEM_NIL"
+  "ALG_SORTED_PREFIXFREE_EQUALITY" > "HOL4Prob.prob_canon.ALG_SORTED_PREFIXFREE_EQUALITY"
+  "ALG_SORTED_MONO" > "HOL4Prob.prob_canon.ALG_SORTED_MONO"
+  "ALG_SORTED_MIN" > "HOL4Prob.prob_canon.ALG_SORTED_MIN"
+  "ALG_SORTED_FILTER" > "HOL4Prob.prob_canon.ALG_SORTED_FILTER"
+  "ALG_SORTED_DEF_ALT" > "HOL4Prob.prob_canon.ALG_SORTED_DEF_ALT"
+  "ALG_SORTED_APPEND" > "HOL4Prob.prob_canon.ALG_SORTED_APPEND"
+  "ALG_PREFIXFREE_TLS" > "HOL4Prob.prob_canon.ALG_PREFIXFREE_TLS"
+  "ALG_PREFIXFREE_TL" > "HOL4Prob.prob_canon.ALG_PREFIXFREE_TL"
+  "ALG_PREFIXFREE_STEP" > "HOL4Prob.prob_canon.ALG_PREFIXFREE_STEP"
+  "ALG_PREFIXFREE_MONO" > "HOL4Prob.prob_canon.ALG_PREFIXFREE_MONO"
+  "ALG_PREFIXFREE_FILTER" > "HOL4Prob.prob_canon.ALG_PREFIXFREE_FILTER"
+  "ALG_PREFIXFREE_ELT" > "HOL4Prob.prob_canon.ALG_PREFIXFREE_ELT"
+  "ALG_PREFIXFREE_APPEND" > "HOL4Prob.prob_canon.ALG_PREFIXFREE_APPEND"
+  "ALG_ORDER_TRANS" > "HOL4Prob.prob_canon.ALG_ORDER_TRANS"
+  "ALG_ORDER_TOTAL" > "HOL4Prob.prob_canon.ALG_ORDER_TOTAL"
+  "ALG_ORDER_SNOC" > "HOL4Prob.prob_canon.ALG_ORDER_SNOC"
+  "ALG_ORDER_REFL" > "HOL4Prob.prob_canon.ALG_ORDER_REFL"
+  "ALG_ORDER_PREFIX_TRANS" > "HOL4Prob.prob_canon.ALG_ORDER_PREFIX_TRANS"
+  "ALG_ORDER_PREFIX_MONO" > "HOL4Prob.prob_canon.ALG_ORDER_PREFIX_MONO"
+  "ALG_ORDER_PREFIX_ANTI" > "HOL4Prob.prob_canon.ALG_ORDER_PREFIX_ANTI"
+  "ALG_ORDER_PREFIX" > "HOL4Prob.prob_canon.ALG_ORDER_PREFIX"
+  "ALG_ORDER_NIL" > "HOL4Prob.prob_canon.ALG_ORDER_NIL"
+  "ALG_ORDER_ANTISYM" > "HOL4Prob.prob_canon.ALG_ORDER_ANTISYM"
+  "ALG_LONGEST_TLS" > "HOL4Prob.prob_canon.ALG_LONGEST_TLS"
+  "ALG_LONGEST_TL" > "HOL4Prob.prob_canon.ALG_LONGEST_TL"
+  "ALG_LONGEST_HD" > "HOL4Prob.prob_canon.ALG_LONGEST_HD"
+  "ALG_LONGEST_APPEND" > "HOL4Prob.prob_canon.ALG_LONGEST_APPEND"
+  "ALG_CANON_SORTED_PREFIXFREE_TWINFREE" > "HOL4Prob.prob_canon.ALG_CANON_SORTED_PREFIXFREE_TWINFREE"
+  "ALG_CANON_PREFS_SORTED" > "HOL4Prob.prob_canon.ALG_CANON_PREFS_SORTED"
+  "ALG_CANON_PREFS_PREFIXFREE" > "HOL4Prob.prob_canon.ALG_CANON_PREFS_PREFIXFREE"
+  "ALG_CANON_PREFS_HD" > "HOL4Prob.prob_canon.ALG_CANON_PREFS_HD"
+  "ALG_CANON_PREFS_DELETES" > "HOL4Prob.prob_canon.ALG_CANON_PREFS_DELETES"
+  "ALG_CANON_PREFS_CONSTANT" > "HOL4Prob.prob_canon.ALG_CANON_PREFS_CONSTANT"
+  "ALG_CANON_MERGE_SORTED_PREFIXFREE_TWINFREE" > "HOL4Prob.prob_canon.ALG_CANON_MERGE_SORTED_PREFIXFREE_TWINFREE"
+  "ALG_CANON_MERGE_SHORTENS" > "HOL4Prob.prob_canon.ALG_CANON_MERGE_SHORTENS"
+  "ALG_CANON_MERGE_PREFIXFREE_PRESERVE" > "HOL4Prob.prob_canon.ALG_CANON_MERGE_PREFIXFREE_PRESERVE"
+  "ALG_CANON_MERGE_CONSTANT" > "HOL4Prob.prob_canon.ALG_CANON_MERGE_CONSTANT"
+  "ALG_CANON_IDEMPOT" > "HOL4Prob.prob_canon.ALG_CANON_IDEMPOT"
+  "ALG_CANON_FIND_SORTED" > "HOL4Prob.prob_canon.ALG_CANON_FIND_SORTED"
+  "ALG_CANON_FIND_PREFIXFREE" > "HOL4Prob.prob_canon.ALG_CANON_FIND_PREFIXFREE"
+  "ALG_CANON_FIND_HD" > "HOL4Prob.prob_canon.ALG_CANON_FIND_HD"
+  "ALG_CANON_FIND_DELETES" > "HOL4Prob.prob_canon.ALG_CANON_FIND_DELETES"
+  "ALG_CANON_FIND_CONSTANT" > "HOL4Prob.prob_canon.ALG_CANON_FIND_CONSTANT"
+  "ALG_CANON_CONSTANT" > "HOL4Prob.prob_canon.ALG_CANON_CONSTANT"
+  "ALG_CANON_BASIC" > "HOL4Prob.prob_canon.ALG_CANON_BASIC"
+  "ALG_CANON2_SORTED_PREFIXFREE_TWINFREE" > "HOL4Prob.prob_canon.ALG_CANON2_SORTED_PREFIXFREE_TWINFREE"
+  "ALG_CANON2_SHORTENS" > "HOL4Prob.prob_canon.ALG_CANON2_SHORTENS"
+  "ALG_CANON2_PREFIXFREE_PRESERVE" > "HOL4Prob.prob_canon.ALG_CANON2_PREFIXFREE_PRESERVE"
+  "ALG_CANON2_CONSTANT" > "HOL4Prob.prob_canon.ALG_CANON2_CONSTANT"
+  "ALG_CANON1_SORTED" > "HOL4Prob.prob_canon.ALG_CANON1_SORTED"
+  "ALG_CANON1_PREFIXFREE" > "HOL4Prob.prob_canon.ALG_CANON1_PREFIXFREE"
+  "ALG_CANON1_CONSTANT" > "HOL4Prob.prob_canon.ALG_CANON1_CONSTANT"
+  "ALGEBRA_CANON_TLS" > "HOL4Prob.prob_canon.ALGEBRA_CANON_TLS"
+  "ALGEBRA_CANON_TL" > "HOL4Prob.prob_canon.ALGEBRA_CANON_TL"
+  "ALGEBRA_CANON_STEP2" > "HOL4Prob.prob_canon.ALGEBRA_CANON_STEP2"
+  "ALGEBRA_CANON_STEP1" > "HOL4Prob.prob_canon.ALGEBRA_CANON_STEP1"
+  "ALGEBRA_CANON_STEP" > "HOL4Prob.prob_canon.ALGEBRA_CANON_STEP"
+  "ALGEBRA_CANON_NIL_MEM" > "HOL4Prob.prob_canon.ALGEBRA_CANON_NIL_MEM"
+  "ALGEBRA_CANON_INDUCTION" > "HOL4Prob.prob_canon.ALGEBRA_CANON_INDUCTION"
+  "ALGEBRA_CANON_DEF_ALT" > "HOL4Prob.prob_canon.ALGEBRA_CANON_DEF_ALT"
+  "ALGEBRA_CANON_CASES_THM" > "HOL4Prob.prob_canon.ALGEBRA_CANON_CASES_THM"
+  "ALGEBRA_CANON_CASES" > "HOL4Prob.prob_canon.ALGEBRA_CANON_CASES"
+  "ALGEBRA_CANON_BASIC" > "HOL4Prob.prob_canon.ALGEBRA_CANON_BASIC"
+
+end